src/ZF/subset.ML
changeset 1461 6bcb44e4d6e5
parent 782 200a16083201
child 1745 6040ec66e1e4
equal deleted inserted replaced
1460:5a6f2aabd538 1461:6bcb44e4d6e5
     1 (*  Title: 	ZF/subset
     1 (*  Title:      ZF/subset
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1991  University of Cambridge
     4     Copyright   1991  University of Cambridge
     5 
     5 
     6 Derived rules involving subsets
     6 Derived rules involving subsets
     7 Union and Intersection as lattice operations
     7 Union and Intersection as lattice operations
     8 *)
     8 *)
   191 qed "RepFun_subset";
   191 qed "RepFun_subset";
   192 
   192 
   193 (*A more powerful claset for subset reasoning*)
   193 (*A more powerful claset for subset reasoning*)
   194 val subset_cs = subset0_cs 
   194 val subset_cs = subset0_cs 
   195   addSIs [subset_refl,cons_subsetI,subset_consI,Union_least,UN_least,Un_least,
   195   addSIs [subset_refl,cons_subsetI,subset_consI,Union_least,UN_least,Un_least,
   196 	  Inter_greatest,Int_greatest,RepFun_subset]
   196           Inter_greatest,Int_greatest,RepFun_subset]
   197   addSIs [Un_upper1,Un_upper2,Int_lower1,Int_lower2]
   197   addSIs [Un_upper1,Un_upper2,Int_lower1,Int_lower2]
   198   addIs  [Union_upper,Inter_lower]
   198   addIs  [Union_upper,Inter_lower]
   199   addSEs [cons_subsetE];
   199   addSEs [cons_subsetE];
   200 
   200