added if_cancel later to simpset
authoroheimb
Wed Nov 27 13:13:21 1996 +0100 (1996-11-27)
changeset 2250891eb76b8045
parent 2249 2af17dd5479e
child 2251 e0e3836f333d
added if_cancel later to simpset
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/simpdata.ML	Wed Nov 27 13:04:04 1996 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Wed Nov 27 13:13:21 1996 +0100
     1.3 @@ -298,8 +298,7 @@
     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, if_cancel,
     1.8 -		 o_apply, imp_disjL, conj_assoc, disj_assoc,
     1.9 +      addsimps ([if_True, if_False, 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];
    1.13 @@ -331,7 +330,7 @@
    1.14  
    1.15  (*** Install simpsets and datatypes in theory structure ***)
    1.16  
    1.17 -simpset := HOL_ss;
    1.18 +simpset := HOL_ss addsimps [if_cancel];
    1.19  
    1.20  exception SS_DATA of simpset;
    1.21