src/ZF/simpdata.ML
changeset 1612 f9f0145e1c7e
parent 1461 6bcb44e4d6e5
child 1791 6b38717439c6
     1.1 --- a/src/ZF/simpdata.ML	Tue Mar 26 11:50:40 1996 +0100
     1.2 +++ b/src/ZF/simpdata.ML	Tue Mar 26 11:58:59 1996 +0100
     1.3 @@ -71,7 +71,9 @@
     1.4     ("op Int",   [IntD1,IntD2])];
     1.5  
     1.6  val ZF_simps = 
     1.7 -    [empty_subsetI, consI1, succI1, ball_simp, if_true, if_false, 
     1.8 +    [empty_subsetI, consI1, cons_not_0, cons_not_0 RS not_sym,
     1.9 +     succI1, succ_not_0, succ_not_0 RS not_sym, succ_inject_iff,
    1.10 +     ball_simp, if_true, if_false, 
    1.11       beta, eta, restrict, fst_conv, snd_conv, split, Pair_iff, singleton_iff,
    1.12       Sigma_empty1, Sigma_empty2, triv_RepFun, subset_refl];
    1.13