ALL_THEN
Thm_cont.ALL_THEN : thm_tactical
Passes a theorem unchanged to a theorem-tactic.
For any theorem-tactic ttac and theorem th, the application
ALL_THEN ttac th results simply in ttac th, that is, the theorem is
passed unchanged to the theorem-tactic. ALL_THEN is the identity
theorem-tactical.
Failure
The application of ALL_THEN to a theorem-tactic never fails. The
resulting theorem-tactic fails under exactly the same conditions as the
original one.
Writing compound tactics or tacticals, e.g. terminating list iterations of theorem-tacticals.
See also
Tactical.ALL_TAC,
Tactical.FAIL_TAC,
Tactical.NO_TAC,
Thm_cont.NO_THEN,
Thm_cont.THEN_TCL,
Thm_cont.ORELSE_TCL