author | paulson |
Wed, 15 May 1996 13:51:15 +0200 | |
changeset 1745 | 6040ec66e1e4 |
parent 1744 | 115e928ad367 |
child 1746 | f0c6aabc6c02 |
src/ZF/subset.ML | file | annotate | diff | comparison | revisions |
--- a/src/ZF/subset.ML Fri May 10 17:41:10 1996 +0200 +++ b/src/ZF/subset.ML Wed May 15 13:51:15 1996 +0200 @@ -157,8 +157,7 @@ qed_goal "Int_lower2" ZF.thy "A Int B <= B" (fn _ => [ (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1)) ]); -qed_goal "Int_greatest" ZF.thy - "!!A B C. [| C<=A; C<=B |] ==> C <= A Int B" +qed_goal "Int_greatest" ZF.thy "!!A B C. [| C<=A; C<=B |] ==> C <= A Int B" (fn prems=> [ (rtac (Int_subset_iff RS iffD2) 1), (REPEAT (ares_tac [conjI] 1)) ]);