changeset 43 | 424c7b1489df |
parent 40 | ac7b7003f177 |
child 57 | 194d088c1511 |
--- 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];