EVERY_TCL : thm_tactical list -> thm_tactical
Composes a list of theorem-tacticals.
When given a list of theorem-tacticals and a theorem, EVERY_TCL simply
composes their effects on the theorem. The effect is:
In other words, if:
EVERY_TCL [ttl1;...;ttln] = ttl1 THEN_TCL ... THEN_TCL ttln
ttl1 ttac th1 = ttac th2 ... ttln ttac thn = ttac thn'
If the theorem-tactical list is empty, the resulting theorem-tactical
behaves in the same way as ALL_THEN, the identity theorem-tactical.
EVERY_TCL [ttl1;...;ttln] ttac th1 = ttac thn'
- FAILURE CONDITIONS
The application to a list of theorem-tacticals never fails.
- SEE ALSO
FIRST_TCL, ORELSE_TCL, REPEAT_TCL, THEN_TCL.