- SYNOPSIS
-
Passes a theorem unchanged to a theorem-tactic.
- DESCRIPTION
-
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 CONDITIONS
-
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
- USES
-
Writing compound tactics or tacticals, e.g. terminating list iterations
of theorem-tacticals.
- SEE ALSO
-
ALL_TAC, FAIL_TAC, NO_TAC, NO_THEN, THEN_TCL, ORELSE_TCL.