author | nipkow |
Wed, 05 Jan 1994 19:41:37 +0100 | |
changeset 215 | bc439e9ce958 |
parent 214 | ed6a3e2b1a33 |
child 216 | 4a10bc05210a |
--- 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];