updated solver of FOL_ss. see change of HOL/simpdata.ML
authornipkow
Wed, 05 Jan 1994 19:41:37 +0100
changeset 215 bc439e9ce958
parent 214 ed6a3e2b1a33
child 216 4a10bc05210a
updated solver of FOL_ss. see change of HOL/simpdata.ML
src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Wed Jan 05 19:33:56 1994 +0100
+++ b/src/FOL/simpdata.ML	Wed Jan 05 19:41:37 1994 +0100
@@ -93,7 +93,8 @@
 val IFOL_ss = empty_ss
       setmksimps mk_rew_rules
       setsolver
-        (fn prems => resolve_tac (TrueI::refl::iff_refl::notFalseI::prems))
+        (fn prems => resolve_tac (TrueI::refl::iff_refl::notFalseI::prems)
+                     ORELSE' atac)
       setsubgoaler asm_simp_tac
       addsimps IFOL_rews
       addcongs [imp_cong];