src/ZF/subset.ML
changeset 1745 6040ec66e1e4
parent 1461 6bcb44e4d6e5
child 2469 b50b8c0eec01
equal deleted inserted replaced
1744:115e928ad367 1745:6040ec66e1e4
   155  (fn _ => [ (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1)) ]);
   155  (fn _ => [ (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1)) ]);
   156 
   156 
   157 qed_goal "Int_lower2" ZF.thy "A Int B <= B"
   157 qed_goal "Int_lower2" ZF.thy "A Int B <= B"
   158  (fn _ => [ (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1)) ]);
   158  (fn _ => [ (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1)) ]);
   159 
   159 
   160 qed_goal "Int_greatest" ZF.thy
   160 qed_goal "Int_greatest" ZF.thy "!!A B C. [| C<=A;  C<=B |] ==> C <= A Int B"
   161                              "!!A B C. [| C<=A;  C<=B |] ==> C <= A Int B"
       
   162  (fn prems=>
   161  (fn prems=>
   163   [ (rtac (Int_subset_iff RS iffD2) 1),
   162   [ (rtac (Int_subset_iff RS iffD2) 1),
   164     (REPEAT (ares_tac [conjI] 1)) ]);
   163     (REPEAT (ares_tac [conjI] 1)) ]);
   165 
   164 
   166 (*** Set difference *)
   165 (*** Set difference *)