# HG changeset patch
# User lcp
# Date 783859924 -3600
# Node ID 527902f96cf2ed098442986d84d8d50a19247de2
# Parent  8fe0fbd768870a7b4ee7f7cf645e35fcc0fb7ff6
ZF/Fixedpt/subset0_cs: moved to ZF/ZF.ML
ZF/Fixedpt/subset_cs: moved to ZF/subset.ML

diff -r 8fe0fbd76887 -r 527902f96cf2 src/ZF/Fixedpt.ML
--- a/src/ZF/Fixedpt.ML	Thu Nov 03 11:45:41 1994 +0100
+++ b/src/ZF/Fixedpt.ML	Thu Nov 03 11:52:04 1994 +0100
@@ -71,20 +71,6 @@
 by (rtac lfp_subset 1);
 val def_lfp_subset = result();
 
-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];
-
-val subset_cs = subset0_cs 
-  addSIs [subset_refl,cons_subsetI,subset_consI,Union_least,UN_least,Un_least,
-	  Inter_greatest,Int_greatest,RepFun_subset]
-  addSIs [Un_upper1,Un_upper2,Int_lower1,Int_lower2]
-  addIs  [Union_upper,Inter_lower]
-  addSEs [cons_subsetE];
-
 val prems = goalw Fixedpt.thy [lfp_def]
     "[| h(D) <= D;  !!X. [| h(X) <= X;  X<=D |] ==> A<=X |] ==> \
 \    A <= lfp(D,h)";