# HG changeset patch
# User paulson
# Date 832161075 -7200
# Node ID 6040ec66e1e4a092dfb95706f06072ab89bab7e0
# Parent  115e928ad36719744e12d2005900f986b1481d42
Deleted spurious line break

diff -r 115e928ad367 -r 6040ec66e1e4 src/ZF/subset.ML
--- 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)) ]);