STRIP_ASSUME_TAC : thm_tactic
A ?- t ====================== STRIP_ASSUME_TAC (A' |- v1 /\ ... /\ vn) A u {v1,...,vn} ?- t A ?- t ================================= STRIP_ASSUME_TAC (A' |- v1 \/ ... \/ vn) A u {v1} ?- t ... A u {vn} ?- t A ?- t ==================== STRIP_ASSUME_TAC (A' |- ?x.v) A u {v[x'/x]} ?- t
# g `m = 0 + m`;;
# e(STRIP_ASSUME_TAC ADD_CLAUSES);; val it : goalstack = 1 subgoal (1 total) 0 [`!n. 0 + n = n`] 1 [`!m. m + 0 = m`] 2 [`!m n. SUC m + n = SUC (m + n)`] 3 [`!m n. m + SUC n = SUC (m + n)`] `m = 0 + m`
?- !m. 0 + m = m