equal
deleted
inserted
replaced
39 |
39 |
40 fun mk_primcorec_assumption_tac ctxt discIs = |
40 fun mk_primcorec_assumption_tac ctxt discIs = |
41 SELECT_GOAL (unfold_thms_tac ctxt |
41 SELECT_GOAL (unfold_thms_tac ctxt |
42 @{thms not_not not_False_eq_True not_True_eq_False de_Morgan_conj de_Morgan_disj} THEN |
42 @{thms not_not not_False_eq_True not_True_eq_False de_Morgan_conj de_Morgan_disj} THEN |
43 SOLVE (HEADGOAL (REPEAT o (rtac refl ORELSE' atac ORELSE' etac conjE ORELSE' |
43 SOLVE (HEADGOAL (REPEAT o (rtac refl ORELSE' atac ORELSE' etac conjE ORELSE' |
|
44 eresolve_tac falseEs ORELSE' |
44 resolve_tac @{thms TrueI conjI disjI1 disjI2} ORELSE' |
45 resolve_tac @{thms TrueI conjI disjI1 disjI2} ORELSE' |
45 dresolve_tac discIs THEN' atac ORELSE' |
46 dresolve_tac discIs THEN' atac ORELSE' |
46 etac notE THEN' atac ORELSE' |
47 etac notE THEN' atac ORELSE' |
47 etac disjE)))); |
48 etac disjE)))); |
48 |
49 |