# HG changeset patch
# User lcp
# Date 783862255 -3600
# Node ID bf95dada47acd21198ebaddeba33a119a738bec7
# Parent  4dddc8d0c384c47de15828b2eee2cdedd8bb0fce
ZF/Fixedpt/subset_cs: moved to ZF/subset.ML

diff -r 4dddc8d0c384 -r bf95dada47ac src/ZF/subset.ML
--- a/src/ZF/subset.ML	Thu Nov 03 12:26:59 1994 +0100
+++ b/src/ZF/subset.ML	Thu Nov 03 12:30:55 1994 +0100
@@ -189,3 +189,12 @@
 by (etac ssubst 1);
 by (eresolve_tac prems 1);
 val RepFun_subset = result();
+
+(*A more powerful claset for subset reasoning*)
+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];
+