# HG changeset patch
# User lcp
# Date 783862019 -3600
# Node ID 4dddc8d0c384c47de15828b2eee2cdedd8bb0fce
# Parent  91bc4b9eee1d58fb8324b2850e0010ee140f6311
ZF/Fixedpt/subset0_cs: moved to ZF/ZF.ML

diff -r 91bc4b9eee1d -r 4dddc8d0c384 src/ZF/ZF.ML
--- a/src/ZF/ZF.ML	Thu Nov 03 12:23:19 1994 +0100
+++ b/src/ZF/ZF.ML	Thu Nov 03 12:26:59 1994 +0100
@@ -61,6 +61,7 @@
   val separation	: thm
   val setup_induction	: thm
   val set_mp_tac	: int -> tactic
+  val subset0_cs	: claset
   val subsetCE		: thm
   val subsetD		: thm
   val subsetI		: thm
@@ -466,12 +467,16 @@
  (fn [major,minor]=>
   [ (rtac (minor RS (major RS equalityD1 RS subsetD RS emptyE)) 1) ]);
 
-val lemmas_cs = FOL_cs
-  addSIs [ballI, InterI, CollectI, PowI, subsetI]
+(*A claset that leaves <= formulae unchanged!*)
+val subset0_cs = FOL_cs
+  addSIs [ballI, InterI, CollectI, PowI, empty_subsetI]
   addIs [bexI, UnionI, ReplaceI, RepFunI]
   addSEs [bexE, make_elim PowD, UnionE, ReplaceE2, RepFunE,
 	  CollectE, emptyE]
-  addEs [rev_ballE, InterD, make_elim InterD, subsetD, subsetCE];
+  addEs [rev_ballE, InterD, make_elim InterD, subsetD];
+
+(*Standard claset*)
+val lemmas_cs = subset0_cs addSIs [subsetI] addEs [subsetCE];
 
 (*Lemma for the inductive definition in Zorn.thy*)
 val Union_in_Pow = prove_goal ZF.thy