# HG changeset patch
# User blanchet
# Date 1381870501 -7200
# Node ID 32730ba3ab850e621ef0ee8e703d2024aef9b976
# Parent  ba709c93447006e8c00cbf814559e2800d0f1320
strengthened tactic to deal with 'False ==> ...'

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