STRIP_GOAL_THEN : thm_tactic -> tactic
A ?- !x.u ============== STRIP_GOAL_THEN ttac A ?- u[x'/x]
A ?- v /\ w ================= STRIP_GOAL_THEN ttac A ?- v A ?- w
A ?- v =============== ttac (u |- u) A' ?- v'
A ?- u ==> v ==================== STRIP_GOAL_THEN ttac A' ?- v'
# g `n = 1 ==> n * n = n`;; Warning: Free variables in goal: n val it : goalstack = 1 subgoal (1 total) `n = 1 ==> n * n = n`
# e(STRIP_GOAL_THEN SUBST1_TAC);; val it : goalstack = 1 subgoal (1 total) `1 * 1 = 1`