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