$ : ('a -> 'b) * 'a -> 'b

- STRUCTURE
- SYNOPSIS
- Right-associated infix function application operator
- DESCRIPTION
- Writing f $ x is another way of writing f x.
- FAILURE
- Fails if f x would fail.
- COMMENTS
- Because $ is right-associated, this can be a convenient way to avoid parentheses. For example,instead of
first_x_assum $ qspec_then ‘m’ $ qx_choose_then ‘z’ strip_assume_tac

Note also that $ is tighter than the various THEN infixes, so a tactic such as the one above can be used in a proof without needing protection by extra parentheses.first_x_assum (qspec_then ‘m’ (qx_choose_then ‘z’ strip_assume_tac))

HOL Kananaskis-14