# HG changeset patch # User nipkow # Date 757795297 -3600 # Node ID bc439e9ce95866ad24ab7795a43de8187a2b79e9 # Parent ed6a3e2b1a33bffd1b1e9aad4fdd58145cc7f467 updated solver of FOL_ss. see change of HOL/simpdata.ML diff -r ed6a3e2b1a33 -r bc439e9ce958 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];