added etac FalseE to the simplifier's solver.
authornipkow
Tue, 15 Feb 1994 07:55:22 +0100
changeset 43 424c7b1489df
parent 42 87f6e8b93221
child 44 64eda8afe2b4
added etac FalseE to the simplifier's solver.
simpdata.ML
--- a/simpdata.ML	Sat Feb 12 14:46:21 1994 +0100
+++ b/simpdata.ML	Tue Feb 15 07:55:22 1994 +0100
@@ -94,7 +94,8 @@
 
 val HOL_ss = empty_ss
       setmksimps mk_rews
-      setsolver (fn prems => resolve_tac (TrueI::refl::prems) ORELSE' atac)
+      setsolver (fn prems => resolve_tac (TrueI::refl::prems) ORELSE' atac
+                             ORELSE' etac FalseE)
       setsubgoaler asm_simp_tac
       addsimps ([if_True, if_False, o_apply, conj_assoc] @ simp_thms)
       addcongs [imp_cong];