# HG changeset patch
# User paulson
# Date 827837939 -3600
# Node ID f9f0145e1c7ed432f99981ce5f76cecf753a7659
# Parent  35e0fd1b17754ea9882c57da30124417d3f738d6
Added new rewrite rules about cons and succ

diff -r 35e0fd1b1775 -r f9f0145e1c7e src/ZF/simpdata.ML
--- a/src/ZF/simpdata.ML	Tue Mar 26 11:50:40 1996 +0100
+++ b/src/ZF/simpdata.ML	Tue Mar 26 11:58:59 1996 +0100
@@ -71,7 +71,9 @@
    ("op Int",   [IntD1,IntD2])];
 
 val ZF_simps = 
-    [empty_subsetI, consI1, succI1, ball_simp, if_true, if_false, 
+    [empty_subsetI, consI1, cons_not_0, cons_not_0 RS not_sym,
+     succI1, succ_not_0, succ_not_0 RS not_sym, succ_inject_iff,
+     ball_simp, if_true, if_false, 
      beta, eta, restrict, fst_conv, snd_conv, split, Pair_iff, singleton_iff,
      Sigma_empty1, Sigma_empty2, triv_RepFun, subset_refl];