# HG changeset patch
# User paulson
# Date 909661353 -3600
# Node ID c675d4a8c26aba57ac6e212e008fb99f6d0dea53
# Parent  af3eb75b11e599d1e9ec8c83594150cd4e2c6c38
tidied

diff -r af3eb75b11e5 -r c675d4a8c26a src/ZF/Zorn.ML
--- a/src/ZF/Zorn.ML	Thu Oct 29 12:41:45 1998 +0100
+++ b/src/ZF/Zorn.ML	Thu Oct 29 12:42:33 1998 +0100
@@ -13,12 +13,11 @@
 
 (*** Section 1.  Mathematical Preamble ***)
 
-Goal "!!A B C. (ALL x:C. x<=A | B<=x) ==> Union(C)<=A | B<=Union(C)";
+Goal "(ALL x:C. x<=A | B<=x) ==> Union(C)<=A | B<=Union(C)";
 by (Blast_tac 1);
 qed "Union_lemma0";
 
-Goal
-    "!!A B C. [| c:C; ALL x:C. A<=x | x<=B |] ==> A<=Inter(C) | Inter(C)<=B";
+Goal "[| c:C; ALL x:C. A<=x | x<=B |] ==> A<=Inter(C) | Inter(C)<=B";
 by (Blast_tac 1);
 qed "Inter_lemma0";