help : string -> unit
# help "lhs";; ------------------------------------------------------------------- lhs : term -> term SYNOPSIS Returns the left-hand side of an equation. DESCRIPTION lhs `t1 = t2` returns `t1`. FAILURE CONDITIONS Fails with lhs if the term is not an equation. EXAMPLES # lhs `2 + 2 = 4`;; val it : term = `2 + 2` SEE ALSO dest_eq, lhand, rand, rhs. ------------------------------------------------------------------- val it : unit = ()
# help "IMP_TAC";; ------------------------------------------------------------------- No help found for "IMP_TAC"; did you mean: help "SIMP_TAC";; help "MP_TAC";; help "IMP_TRANS";; ? --------------------------------------------------------------------