if_cancel added to HOL_ss
authoroheimb
Tue Nov 26 17:49:25 1996 +0100 (1996-11-26)
changeset 2234041bf27011b1
parent 2233 f919bdd5f9b6
child 2235 866dbb04816c
if_cancel added to HOL_ss
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/simpdata.ML	Tue Nov 26 16:57:13 1996 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Tue Nov 26 17:49:25 1996 +0100
     1.3 @@ -298,7 +298,8 @@
     1.4        setsolver (fn prems => resolve_tac (TrueI::refl::prems) ORELSE' atac
     1.5                               ORELSE' etac FalseE)
     1.6        setsubgoaler asm_simp_tac
     1.7 -      addsimps ([if_True, if_False, o_apply, imp_disjL, conj_assoc, disj_assoc,
     1.8 +      addsimps ([if_True, if_False, if_cancel,
     1.9 +		 o_apply, imp_disjL, conj_assoc, disj_assoc,
    1.10                   de_Morgan_conj, de_Morgan_disj, not_all, not_ex, cases_simp]
    1.11          @ ex_simps @ all_simps @ simp_thms)
    1.12        addcongs [imp_cong];