$ : ('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,
   first_x_assum $ qspec_then ‘m’ $ qx_choose_then ‘z’ strip_assume_tac
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.
HOL  Trindemossen-1