# HG changeset patch
# User lcp
# Date 789876187 -3600
# Node ID 4c8d0ece1f958bb0c81777233d6fcc669bf6cfa3
# Parent  2e3ca37dfa141e835ef56923db57e0bf7cdccab6
Added singleton_iff, Sigma_empty1, Sigma_empty2, Collect_simps
and UnInt_simps to ZF_ss.  Added consI1 to ZF_typechecks.

diff -r 2e3ca37dfa14 -r 4c8d0ece1f95 src/ZF/simpdata.ML
--- a/src/ZF/simpdata.ML	Thu Jan 12 03:02:34 1995 +0100
+++ b/src/ZF/simpdata.ML	Thu Jan 12 03:03:07 1995 +0100
@@ -24,7 +24,8 @@
 
 fun typechk_tac tyrls = REPEAT (typechk_step_tac tyrls);
 
-val ZF_typechecks = [if_type,lam_type,SigmaI,apply_type,split_type];
+val ZF_typechecks =
+    [if_type, lam_type, SigmaI, apply_type, split_type, consI1];
 
 (*Instantiates variables in typing conditions.
   drawback: does not simplify conjunctions*)
@@ -68,9 +69,10 @@
      | _                       => [th]
   end;
 
-val ZF_simps = [empty_subsetI, consI1, succI1, ball_simp, if_true, if_false, 
-		beta, eta, restrict, fst_conv, snd_conv, split, Pair_iff,
-		triv_RepFun, subset_refl];
+val ZF_simps = 
+    [empty_subsetI, consI1, succI1, 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];
 
 (*Sigma_cong, Pi_cong NOT included by default since they cause
   flex-flex pairs and the "Check your prover" error -- because most
@@ -80,5 +82,6 @@
 
 val ZF_ss = FOL_ss 
       setmksimps (map mk_meta_eq o atomize o gen_all)
-      addsimps (ZF_simps @ mem_simps @ bquant_simps)
+      addsimps (ZF_simps @ mem_simps @ bquant_simps @ 
+		Collect_simps @ UnInt_simps)
       addcongs ZF_congs;