1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML Tue Oct 15 17:21:16 2013 +0200
1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML Tue Oct 15 22:55:01 2013 +0200
1.3 @@ -41,6 +41,7 @@
1.4 SELECT_GOAL (unfold_thms_tac ctxt
1.5 @{thms not_not not_False_eq_True not_True_eq_False de_Morgan_conj de_Morgan_disj} THEN
1.6 SOLVE (HEADGOAL (REPEAT o (rtac refl ORELSE' atac ORELSE' etac conjE ORELSE'
1.7 + eresolve_tac falseEs ORELSE'
1.8 resolve_tac @{thms TrueI conjI disjI1 disjI2} ORELSE'
1.9 dresolve_tac discIs THEN' atac ORELSE'
1.10 etac notE THEN' atac ORELSE'