Add STRIP_ALL_THEN and CHOOSE_ALL_THEN

Open ordinarymath opened this issue 2 months ago • 1 comments

Only STRIP_ALL_THEN is exposed in the signature.

STRIP_ALL_THEN should behave like REPEAT_TCL STRIP_THM_THEN and CHOOSE_ALL_THEN should behave like REPEAT_TCL CHOOSE_THEN

This change is intended to speedup record construction time where STRIP_ALL_THEN is being called via STRUCT_CASES_TAC

Oct 27 '25 07:10 ordinarymath

I've figured out why this is way slower than using MP with a induction thm + GENL. https://github.com/HOL-Theorem-Prover/HOL/blob/a902f2db73f6a761d57905ec18eb06291ad8a9b9/src/1/Thm_cont.sml#L104-L133 This bug fix means that the thm passed through the continuation gets bigger and bigger with more hyps and resulting call of CHOOSE has to check for var_occurs for all of the hyps.

Nov 04 '25 04:11 ordinarymath