DEBSOURCES
Skip Quicknav
sources / hol-light / 20120602-1 / Help / then_.doc
1234567891011
\DOC then_ \TYPE {then_ : tactic -> tactic -> tactic} \SYNOPSIS Non-infix version of {THEN}. \SEEALSO THEN. \ENDDOC