src/HOL/Real/Lubs.ML

--- a/src/HOL/Real/Lubs.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Real/Lubs.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -10,34 +10,34 @@
 (*------------------------------------------------------------------------
                         Rules for *<= and <=*
  ------------------------------------------------------------------------*)
-Goalw [setle_def] "!!x. ALL y: S. y <= x ==> S *<= x";
+Goalw [setle_def] "ALL y: S. y <= x ==> S *<= x";
 by (assume_tac 1);
 qed "setleI";
 
-Goalw [setle_def] "!!x. [| S *<= x; y: S |] ==> y <= x";
+Goalw [setle_def] "[| S *<= x; y: S |] ==> y <= x";
 by (Fast_tac 1);
 qed "setleD";
 
-Goalw [setge_def] "!!x. ALL y: S. x<= y ==> x <=* S";
+Goalw [setge_def] "ALL y: S. x<= y ==> x <=* S";
 by (assume_tac 1);
 qed "setgeI";
 
-Goalw [setge_def] "!!x. [| x <=* S; y: S |] ==> x <= y";
+Goalw [setge_def] "[| x <=* S; y: S |] ==> x <= y";
 by (Fast_tac 1);
 qed "setgeD";
 
 (*------------------------------------------------------------------------
                         Rules about leastP, ub and lub
  ------------------------------------------------------------------------*)
-Goalw [leastP_def] "!!x. leastP P x ==> P x";
+Goalw [leastP_def] "leastP P x ==> P x";
 by (Step_tac 1);
 qed "leastPD1";
 
-Goalw [leastP_def] "!!x. leastP P x ==> x <=* Collect P";
+Goalw [leastP_def] "leastP P x ==> x <=* Collect P";
 by (Step_tac 1);
 qed "leastPD2";
 
-Goal "!!x. [| leastP P x; y: Collect P |] ==> x <= y";
+Goal "[| leastP P x; y: Collect P |] ==> x <= y";
 by (blast_tac (claset() addSDs [leastPD2,setgeD]) 1);
 qed "leastPD3";
 
@@ -51,19 +51,19 @@
 by (Step_tac 1);
 qed "isLubD1a";
 
-Goalw [isUb_def] "!!x. isLub R S x ==> isUb R S x";
+Goalw [isUb_def] "isLub R S x ==> isUb R S x";
 by (blast_tac (claset() addDs [isLubD1,isLubD1a]) 1);
 qed "isLub_isUb";
 
-Goal "!!x. [| isLub R S x; y : S |] ==> y <= x";
+Goal "[| isLub R S x; y : S |] ==> y <= x";
 by (blast_tac (claset() addSDs [isLubD1,setleD]) 1);
 qed "isLubD2";
 
-Goalw [isLub_def] "!!x. isLub R S x ==> leastP(isUb R S) x";
+Goalw [isLub_def] "isLub R S x ==> leastP(isUb R S) x";
 by (assume_tac 1);
 qed "isLubD3";
 
-Goalw [isLub_def] "!!x. leastP(isUb R S) x ==> isLub R S x";
+Goalw [isLub_def] "leastP(isUb R S) x ==> isLub R S x";
 by (assume_tac 1);
 qed "isLubI1";
 
@@ -72,27 +72,27 @@
 by (Step_tac 1);
 qed "isLubI2";
 
-Goalw [isUb_def] "!!x. [| isUb R S x; y : S |] ==> y <= x";
+Goalw [isUb_def] "[| isUb R S x; y : S |] ==> y <= x";
 by (fast_tac (claset() addDs [setleD]) 1);
 qed "isUbD";
 
-Goalw [isUb_def] "!!x. isUb R S x ==> S *<= x";
+Goalw [isUb_def] "isUb R S x ==> S *<= x";
 by (Step_tac 1);
 qed "isUbD2";
 
-Goalw [isUb_def] "!!x. isUb R S x ==> x: R";
+Goalw [isUb_def] "isUb R S x ==> x: R";
 by (Step_tac 1);
 qed "isUbD2a";
 
-Goalw [isUb_def] "!!x. [| S *<= x; x: R |] ==> isUb R S x";
+Goalw [isUb_def] "[| S *<= x; x: R |] ==> isUb R S x";
 by (Step_tac 1);
 qed "isUbI";
 
-Goalw [isLub_def] "!!x. [| isLub R S x; isUb R S y |] ==> x <= y";
+Goalw [isLub_def] "[| isLub R S x; isUb R S y |] ==> x <= y";
 by (blast_tac (claset() addSIs [leastPD3]) 1);
 qed "isLub_le_isUb";
 
-Goalw [ubs_def,isLub_def] "!!x. isLub R S x ==> x <=* ubs R S";
+Goalw [ubs_def,isLub_def] "isLub R S x ==> x <=* ubs R S";
 by (etac leastPD2 1);
 qed "isLub_ubs";