src/ZF/subset.ML
changeset 689 bf95dada47ac
parent 0 a5a9c433f639
child 760 f0200e91b272
--- 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];
+