REPEAT_TCL : thm_tactical -> thm_tactical
REPEAT_TCL ttl ttac th
# g `(0 = w /\ 0 = x) /\ 0 = y /\ 0 = z ==> w + x + y + z = 0`;; Warning: Free variables in goal: w, x, y, z val it : goalstack = 1 subgoal (1 total) `(0 = w /\ 0 = x) /\ 0 = y /\ 0 = z ==> w + x + y + z = 0`
# e(DISCH_THEN (REPEAT_TCL CONJUNCTS_THEN (SUBST1_TAC o SYM)) THEN REWRITE_TAC[ADD_CLAUSES]);;