STRIP_ALL_THEN

Thm_cont.STRIP_ALL_THEN : thm_tactical

Splits a theorem into a list of theorems and then calls the resulting theorem tactic on it.

Given a theorem th STRIP_ALL_THEN ttac th splits th into a list of theorems and then applies the ttac on the resulting theorems. This is done by recursively applying STRIP_THM_THEN and then calling the ttac if the theorem can’t be split anymore.

Failure

STRIP_ALL_THEN ttac th fails if the any application of ttac fails, which is applied with the stripped theorems from th.

Comments

STRIP_ALL_THEN behaves exactly like REPEAT_TCL STRIP_THM_THEN but is faster.

See also

Thm_cont.REPEAT_TCL, Thm_cont.STRIP_ALL_THEN, Tactic.STRIP_ASSUME_TAC