Lib.$

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.