--- 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];