# HG changeset patch
# User nipkow
# Date 1101984121 -3600
# Node ID 300e09825d8b64d6d1bd5d7ef08122339efbfd61
# Parent  8bad1f42fec06c0c442f8008b22d857425f820d3
Added "ALL x > y" and relatives.

diff -r 8bad1f42fec0 -r 300e09825d8b src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Dec 02 11:09:19 2004 +0100
+++ b/src/HOL/HOL.thy	Thu Dec 02 11:42:01 2004 +0100
@@ -1109,12 +1109,22 @@
   "_leAll"   :: "[idt, 'a, bool] => bool"   ("(3ALL _<=_./ _)" [0, 0, 10] 10)
   "_leEx"    :: "[idt, 'a, bool] => bool"   ("(3EX _<=_./ _)" [0, 0, 10] 10)
 
+  "_gtAll" :: "[idt, 'a, bool] => bool"   ("(3ALL _>_./ _)"  [0, 0, 10] 10)
+  "_gtEx"  :: "[idt, 'a, bool] => bool"   ("(3EX _>_./ _)"  [0, 0, 10] 10)
+  "_geAll"   :: "[idt, 'a, bool] => bool"   ("(3ALL _>=_./ _)" [0, 0, 10] 10)
+  "_geEx"    :: "[idt, 'a, bool] => bool"   ("(3EX _>=_./ _)" [0, 0, 10] 10)
+
 syntax (xsymbols)
   "_lessAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_<_./ _)"  [0, 0, 10] 10)
   "_lessEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_<_./ _)"  [0, 0, 10] 10)
   "_leAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)
   "_leEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10)
 
+  "_gtAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_>_./ _)"  [0, 0, 10] 10)
+  "_gtEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_>_./ _)"  [0, 0, 10] 10)
+  "_geAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10)
+  "_geEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10)
+
 syntax (HOL)
   "_lessAll" :: "[idt, 'a, bool] => bool"   ("(3! _<_./ _)"  [0, 0, 10] 10)
   "_lessEx"  :: "[idt, 'a, bool] => bool"   ("(3? _<_./ _)"  [0, 0, 10] 10)
@@ -1127,11 +1137,20 @@
   "_leAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)
   "_leEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10)
 
+  "_gtAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_>_./ _)"  [0, 0, 10] 10)
+  "_gtEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_>_./ _)"  [0, 0, 10] 10)
+  "_geAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10)
+  "_geEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10)
+
 translations
  "ALL x<y. P"   =>  "ALL x. x < y --> P"
  "EX x<y. P"    =>  "EX x. x < y  & P"
  "ALL x<=y. P"  =>  "ALL x. x <= y --> P"
  "EX x<=y. P"   =>  "EX x. x <= y & P"
+ "ALL x>y. P"   =>  "ALL x. x > y --> P"
+ "EX x>y. P"    =>  "EX x. x > y  & P"
+ "ALL x>=y. P"  =>  "ALL x. x >= y --> P"
+ "EX x>=y. P"   =>  "EX x. x >= y & P"
 
 print_translation {*
 let
diff -r 8bad1f42fec0 -r 300e09825d8b src/HOL/Hyperreal/HyperPow.thy
--- a/src/HOL/Hyperreal/HyperPow.thy	Thu Dec 02 11:09:19 2004 +0100
+++ b/src/HOL/Hyperreal/HyperPow.thy	Thu Dec 02 11:42:01 2004 +0100
@@ -7,7 +7,7 @@
 header{*Exponentials on the Hyperreals*}
 
 theory HyperPow
-imports HyperArith HyperNat "../Real/RealPow"
+imports HyperArith HyperNat
 begin
 
 instance hypreal :: power ..
diff -r 8bad1f42fec0 -r 300e09825d8b src/HOL/Hyperreal/Integration.thy
--- a/src/HOL/Hyperreal/Integration.thy	Thu Dec 02 11:09:19 2004 +0100
+++ b/src/HOL/Hyperreal/Integration.thy	Thu Dec 02 11:42:01 2004 +0100
@@ -17,13 +17,13 @@
   --{*Partitions and tagged partitions etc.*}
 
   partition :: "[(real*real),nat => real] => bool"
-  "partition == %(a,b) D. ((D 0 = a) &
-                         (\<exists>N. ((\<forall>n. n < N --> D(n) < D(Suc n)) &
-                            (\<forall>n. N \<le> n --> (D(n) = b)))))"
+  "partition == %(a,b) D. D 0 = a &
+                         (\<exists>N. (\<forall>n < N. D(n) < D(Suc n)) &
+                              (\<forall>n \<ge> N. D(n) = b))"
 
   psize :: "(nat => real) => nat"
-  "psize D == @N. (\<forall>n. n < N --> D(n) < D(Suc n)) &
-                  (\<forall>n. N \<le> n --> (D(n) = D(N)))"
+  "psize D == SOME N. (\<forall>n < N. D(n) < D(Suc n)) &
+                      (\<forall>n \<ge> N. D(n) = D(N))"
 
   tpart :: "[(real*real),((nat => real)*(nat =>real))] => bool"
   "tpart == %(a,b) (D,p). partition(a,b) D &
@@ -45,7 +45,7 @@
   --{*Gauge integrability (definite)*}
 
    Integral :: "[(real*real),real=>real,real] => bool"
-   "Integral == %(a,b) f k. \<forall>e. 0 < e -->
+   "Integral == %(a,b) f k. \<forall>e > 0.
                                (\<exists>g. gauge(%x. a \<le> x & x \<le> b) g &
                                (\<forall>D p. tpart(a,b) (D,p) & fine(g)(D,p) -->
                                          \<bar>rsum(D,p) f - k\<bar> < e))"
@@ -70,8 +70,8 @@
 lemma partition:
        "(partition(a,b) D) =
         ((D 0 = a) &
-         (\<forall>n. n < (psize D) --> D n < D(Suc n)) &
-         (\<forall>n. (psize D) \<le> n --> (D n = b)))"
+         (\<forall>n < psize D. D n < D(Suc n)) &
+         (\<forall>n \<ge> psize D. D n = b))"
 apply (simp add: partition_def, auto)
 apply (subgoal_tac [!] "psize D = N", auto)
 apply (simp_all (no_asm) add: psize_def)
@@ -181,13 +181,11 @@
 
 lemma lemma_partition_append1:
      "[| partition (a, b) D1; partition (b, c) D2 |]
-       ==> (\<forall>n.
-             n < psize D1 + psize D2 -->
+       ==> (\<forall>n < psize D1 + psize D2.
              (if n < psize D1 then D1 n else D2 (n - psize D1))
              < (if Suc n < psize D1 then D1 (Suc n)
                 else D2 (Suc n - psize D1))) &
-         (\<forall>n.
-             psize D1 + psize D2 \<le> n -->
+         (\<forall>n \<ge> psize D1 + psize D2.
              (if n < psize D1 then D1 n else D2 (n - psize D1)) =
              (if psize D1 + psize D2 < psize D1 then D1 (psize D1 + psize D2)
               else D2 (psize D1 + psize D2 - psize D1)))"
@@ -412,9 +410,8 @@
                   --> \<bar>(f(v) - f(u)) - (f'(x) * (v - u))\<bar> \<le> e * (v - u))"
 apply (simp add: gauge_def)
 apply (subgoal_tac "\<forall>x. a \<le> x & x \<le> b --> 
-        (\<exists>d. 0 < d & 
-             (\<forall>u v. u \<le> x & x \<le> v & (v - u) < d --> 
-                \<bar>(f (v) - f (u)) - (f' (x) * (v - u))\<bar> \<le> e * (v - u)))")
+        (\<exists>d > 0. \<forall>u v. u \<le> x & x \<le> v & (v - u) < d --> 
+                       \<bar>(f (v) - f (u)) - (f' (x) * (v - u))\<bar> \<le> e * (v - u))")
 apply (drule choiceP, auto)
 apply (drule spec, auto)
 apply (auto simp add: DERIV_iff2 LIM_def)
@@ -445,7 +442,7 @@
 apply (drule order_le_imp_less_or_eq, auto) 
 apply (auto simp add: Integral_def)
 apply (rule ccontr)
-apply (subgoal_tac "\<forall>e. 0 < e --> (\<exists>g. gauge (%x. a \<le> x & x \<le> b) g & (\<forall>D p. tpart (a, b) (D, p) & fine g (D, p) --> \<bar>rsum (D, p) f' - (f b - f a)\<bar> \<le> e))")
+apply (subgoal_tac "\<forall>e > 0. \<exists>g. gauge (%x. a \<le> x & x \<le> b) g & (\<forall>D p. tpart (a, b) (D, p) & fine g (D, p) --> \<bar>rsum (D, p) f' - (f b - f a)\<bar> \<le> e)")
 apply (rotate_tac 3)
 apply (drule_tac x = "e/2" in spec, auto)
 apply (drule spec, auto)
@@ -796,7 +793,7 @@
 lemma lemma_Integral_le:
      "[| \<forall>x. a \<le> x & x \<le> b --> f x \<le> g x;
          tpart(a,b) (D,p)
-      |] ==> \<forall>n. n \<le> psize D --> f (p n) \<le> g (p n)"
+      |] ==> \<forall>n \<le> psize D. f (p n) \<le> g (p n)"
 apply (simp add: tpart_def)
 apply (auto, frule partition [THEN iffD1], auto)
 apply (drule_tac x = "p n" in spec, auto)
@@ -842,12 +839,11 @@
 
 lemma Integral_imp_Cauchy:
      "(\<exists>k. Integral(a,b) f k) ==>
-      (\<forall>e. 0 < e -->
-               (\<exists>g. gauge (%x. a \<le> x & x \<le> b) g &
+      (\<forall>e > 0. \<exists>g. gauge (%x. a \<le> x & x \<le> b) g &
                        (\<forall>D1 D2 p1 p2.
                             tpart(a,b) (D1, p1) & fine g (D1,p1) &
                             tpart(a,b) (D2, p2) & fine g (D2,p2) -->
-                            \<bar>rsum(D1,p1) f - rsum(D2,p2) f\<bar> < e)))"
+                            \<bar>rsum(D1,p1) f - rsum(D2,p2) f\<bar> < e))"
 apply (simp add: Integral_def, auto)
 apply (drule_tac x = "e/2" in spec, auto)
 apply (rule exI, auto)
@@ -862,13 +858,12 @@
 
 lemma Cauchy_iff2:
      "Cauchy X =
-      (\<forall>j. (\<exists>M. \<forall>m n. M \<le> m & M \<le> n -->
-               \<bar>X m + - X n\<bar> < inverse(real (Suc j))))"
+      (\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. \<bar>X m + - X n\<bar> < inverse(real (Suc j))))"
 apply (simp add: Cauchy_def, auto)
 apply (drule reals_Archimedean, safe)
 apply (drule_tac x = n in spec, auto)
 apply (rule_tac x = M in exI, auto)
-apply (drule_tac x = m in spec)
+apply (drule_tac x = m in spec, simp)
 apply (drule_tac x = na in spec, auto)
 done
 
diff -r 8bad1f42fec0 -r 300e09825d8b src/HOL/Hyperreal/Lim.thy
--- a/src/HOL/Hyperreal/Lim.thy	Thu Dec 02 11:09:19 2004 +0100
+++ b/src/HOL/Hyperreal/Lim.thy	Thu Dec 02 11:42:01 2004 +0100
@@ -8,7 +8,7 @@
 header{*Limits, Continuity and Differentiation*}
 
 theory Lim
-imports SEQ RealDef
+imports SEQ
 begin
 
 text{*Standard and Nonstandard Definitions*}
@@ -17,9 +17,8 @@
   LIM :: "[real=>real,real,real] => bool"
 				("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60)
   "f -- a --> L ==
-     \<forall>r. 0 < r -->
-	     (\<exists>s. 0 < s & (\<forall>x. (x \<noteq> a & (\<bar>x + -a\<bar> < s)
-			  --> \<bar>f x + -L\<bar> < r)))"
+     \<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & \<bar>x + -a\<bar> < s
+			  --> \<bar>f x + -L\<bar> < r"
 
   NSLIM :: "[real=>real,real,real] => bool"
 			      ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60)
@@ -58,9 +57,7 @@
 		       inc = ( *f* f)(hypreal_of_real x + h) + -hypreal_of_real (f x))"
 
   isUCont :: "(real=>real) => bool"
-  "isUCont f ==  (\<forall>r. 0 < r -->
-		      (\<exists>s. 0 < s & (\<forall>x y. \<bar>x + -y\<bar> < s
-			    --> \<bar>f x + -f y\<bar> < r)))"
+  "isUCont f ==  \<forall>r > 0. \<exists>s > 0. \<forall>x y. \<bar>x + -y\<bar> < s --> \<bar>f x + -f y\<bar> < r"
 
   isNSUCont :: "(real=>real) => bool"
   "isNSUCont f == (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
@@ -84,12 +81,12 @@
 
 lemma LIM_eq:
      "f -- a --> L =
-     (\<forall>r. 0<r --> (\<exists>s. 0 < s & (\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> \<bar>f x - L\<bar> < r)))"
+     (\<forall>r>0.\<exists>s>0.\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> \<bar>f x - L\<bar> < r)"
 by (simp add: LIM_def diff_minus)
 
 lemma LIM_D:
      "[| f -- a --> L; 0<r |]
-      ==> \<exists>s. 0 < s & (\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> \<bar>f x - L\<bar> < r)"
+      ==> \<exists>s>0.\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> \<bar>f x - L\<bar> < r"
 by (simp add: LIM_eq)
 
 lemma LIM_const [simp]: "(%x. k) -- x --> k"
@@ -111,8 +108,7 @@
     where gs:    "0 < gs"
       and gs_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < gs --> \<bar>g x - M\<bar> < r/2"
   by blast
-  show "\<exists>s. 0 < s \<and>
-            (\<forall>x. x \<noteq> a \<and> \<bar>x-a\<bar> < s \<longrightarrow> \<bar>f x + g x - (L + M)\<bar> < r)"
+  show "\<exists>s>0.\<forall>x. x \<noteq> a \<and> \<bar>x-a\<bar> < s \<longrightarrow> \<bar>f x + g x - (L + M)\<bar> < r"
   proof (intro exI conjI strip)
     show "0 < min fs gs"  by (simp add: fs gs)
     fix x :: real
@@ -143,8 +139,7 @@
 lemma LIM_const_not_eq: "k \<noteq> L ==> ~ ((%x. k) -- a --> L)"
 proof (simp add: linorder_neq_iff LIM_eq, elim disjE)
   assume k: "k < L"
-  show "\<exists>r. 0 < r \<and>
-        (\<forall>s. 0 < s \<longrightarrow> (\<exists>x. (x < a \<or> a < x) \<and> \<bar>x-a\<bar> < s) \<and> \<not> \<bar>k-L\<bar> < r)"
+  show "\<exists>r>0. \<forall>s>0. (\<exists>x. (x < a \<or> a < x) \<and> \<bar>x-a\<bar> < s) \<and> \<not> \<bar>k-L\<bar> < r"
   proof (intro exI conjI strip)
     show "0 < L-k" by (simp add: k compare_rls)
     fix s :: real
@@ -157,8 +152,7 @@
   qed
 next
   assume k: "L < k"
-  show "\<exists>r. 0 < r \<and>
-        (\<forall>s. 0 < s \<longrightarrow> (\<exists>x. (x < a \<or> a < x) \<and> \<bar>x-a\<bar> < s) \<and> \<not> \<bar>k-L\<bar> < r)"
+  show "\<exists>r>0.\<forall>s>0. (\<exists>x. (x < a \<or> a < x) \<and> \<bar>x-a\<bar> < s) \<and> \<not> \<bar>k-L\<bar> < r"
   proof (intro exI conjI strip)
     show "0 < k-L" by (simp add: k compare_rls)
     fix s :: real
@@ -245,8 +239,8 @@
 
 subsubsection{*Limit: The NS definition implies the standard definition.*}
 
-lemma lemma_LIM: "\<forall>s. 0 < s --> (\<exists>xa.  xa \<noteq> x &
-         \<bar>xa + - x\<bar> < s  & r \<le> \<bar>f xa + -L\<bar>)
+lemma lemma_LIM: "\<forall>s>0.\<exists>xa.  xa \<noteq> x &
+         \<bar>xa + - x\<bar> < s  & r \<le> \<bar>f xa + -L\<bar>
       ==> \<forall>n::nat. \<exists>xa.  xa \<noteq> x &
               \<bar>xa + -x\<bar> < inverse(real(Suc n)) & r \<le> \<bar>f xa + -L\<bar>"
 apply clarify
@@ -254,8 +248,7 @@
 done
 
 lemma lemma_skolemize_LIM2:
-     "\<forall>s. 0 < s --> (\<exists>xa.  xa \<noteq> x &
-         \<bar>xa + - x\<bar> < s  & r \<le> \<bar>f xa + -L\<bar>)
+     "\<forall>s>0.\<exists>xa.  xa \<noteq> x & \<bar>xa + - x\<bar> < s  & r \<le> \<bar>f xa + -L\<bar>
       ==> \<exists>X. \<forall>n::nat. X n \<noteq> x &
                 \<bar>X n + -x\<bar> < inverse(real(Suc n)) & r \<le> abs(f (X n) + -L)"
 apply (drule lemma_LIM)
@@ -598,17 +591,15 @@
 apply (drule FreeUltrafilterNat_all, ultra)
 done
 
-lemma lemma_LIMu: "\<forall>s. 0 < s --> (\<exists>z y. \<bar>z + - y\<bar> < s & r \<le> \<bar>f z + -f y\<bar>)
-      ==> \<forall>n::nat. \<exists>z y.
-               \<bar>z + -y\<bar> < inverse(real(Suc n)) &
-               r \<le> \<bar>f z + -f y\<bar>"
+lemma lemma_LIMu: "\<forall>s>0.\<exists>z y. \<bar>z + - y\<bar> < s & r \<le> \<bar>f z + -f y\<bar>
+      ==> \<forall>n::nat. \<exists>z y. \<bar>z + -y\<bar> < inverse(real(Suc n)) & r \<le> \<bar>f z + -f y\<bar>"
 apply clarify
 apply (cut_tac n1 = n 
        in real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive], auto)
 done
 
 lemma lemma_skolemize_LIM2u:
-     "\<forall>s. 0 < s --> (\<exists>z y. \<bar>z + - y\<bar> < s  & r \<le> \<bar>f z + -f y\<bar>)
+     "\<forall>s>0.\<exists>z y. \<bar>z + - y\<bar> < s  & r \<le> \<bar>f z + -f y\<bar>
       ==> \<exists>X Y. \<forall>n::nat.
                abs(X n + -(Y n)) < inverse(real(Suc n)) &
                r \<le> abs(f (X n) + -f (Y n))"
@@ -687,7 +678,7 @@
 subsubsection{*Alternative definition for differentiability*}
 
 lemma LIM_I:
-     "(!!r. 0<r ==> (\<exists>s. 0 < s & (\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> \<bar>f x - L\<bar> < r)))
+     "(!!r. 0<r ==> \<exists>s>0.\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> \<bar>f x - L\<bar> < r)
       ==> f -- a --> L"
 by (simp add: LIM_eq)
 
@@ -1438,7 +1429,7 @@
  apply (drule_tac P = "%d. 0<d --> ?P d" and x = 1 in spec, arith)
 apply (drule_tac x = x in spec)+
 apply simp
-apply (drule_tac P = "%r. ?P r --> (\<exists>s. 0<s & ?Q r s) " and x = "\<bar>y - f x\<bar>" in spec)
+apply (drule_tac P = "%r. ?P r --> (\<exists>s>0. ?Q r s) " and x = "\<bar>y - f x\<bar>" in spec)
 apply safe
 apply simp
 apply (drule_tac x = s in spec, clarify)
@@ -1594,11 +1585,10 @@
 lemma DERIV_left_inc:
   assumes der: "DERIV f x :> l"
       and l:   "0 < l"
-  shows "\<exists>d. 0 < d & (\<forall>h. 0 < h & h < d --> f(x) < f(x + h))"
+  shows "\<exists>d > 0. \<forall>h > 0. h < d --> f(x) < f(x + h)"
 proof -
   from l der [THEN DERIV_D, THEN LIM_D [where r = "l"]]
-  have "\<exists>s. 0 < s \<and>
-              (\<forall>z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < l)"
+  have "\<exists>s > 0. (\<forall>z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < l)"
     by (simp add: diff_minus)
   then obtain s
         where s:   "0 < s"
@@ -1608,7 +1598,7 @@
   proof (intro exI conjI strip)
     show "0<s" .
     fix h::real
-    assume "0 < h \<and> h < s"
+    assume "0 < h" "h < s"
     with all [of h] show "f x < f (x+h)"
     proof (simp add: abs_if pos_less_divide_eq diff_minus [symmetric]
 		split add: split_if_asm)
@@ -1624,11 +1614,10 @@
 lemma DERIV_left_dec:
   assumes der: "DERIV f x :> l"
       and l:   "l < 0"
-  shows "\<exists>d. 0 < d & (\<forall>h. 0 < h & h < d --> f(x) < f(x-h))"
+  shows "\<exists>d > 0. \<forall>h > 0. h < d --> f(x) < f(x-h)"
 proof -
   from l der [THEN DERIV_D, THEN LIM_D [where r = "-l"]]
-  have "\<exists>s. 0 < s \<and>
-              (\<forall>z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < -l)"
+  have "\<exists>s > 0. (\<forall>z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < -l)"
     by (simp add: diff_minus)
   then obtain s
         where s:   "0 < s"
@@ -1638,7 +1627,7 @@
   proof (intro exI conjI strip)
     show "0<s" .
     fix h::real
-    assume "0 < h \<and> h < s"
+    assume "0 < h" "h < s"
     with all [of "-h"] show "f x < f (x-h)"
     proof (simp add: abs_if pos_less_divide_eq diff_minus [symmetric]
 		split add: split_if_asm)
@@ -1662,7 +1651,7 @@
   case less
   from DERIV_left_dec [OF der less]
   obtain d' where d': "0 < d'"
-             and lt: "\<forall>h. 0 < h \<and> h < d' \<longrightarrow> f x < f (x-h)" by blast
+             and lt: "\<forall>h > 0. h < d' \<longrightarrow> f x < f (x-h)" by blast
   from real_lbound_gt_zero [OF d d']
   obtain e where "0 < e \<and> e < d \<and> e < d'" ..
   with lt le [THEN spec [where x="x-e"]]
@@ -1671,7 +1660,7 @@
   case greater
   from DERIV_left_inc [OF der greater]
   obtain d' where d': "0 < d'"
-             and lt: "\<forall>h. 0 < h \<and> h < d' \<longrightarrow> f x < f (x + h)" by blast
+             and lt: "\<forall>h > 0. h < d' \<longrightarrow> f x < f (x + h)" by blast
   from real_lbound_gt_zero [OF d d']
   obtain e where "0 < e \<and> e < d \<and> e < d'" ..
   with lt le [THEN spec [where x="x+e"]]
@@ -1857,7 +1846,7 @@
 lemma DERIV_isconst_end: "[| a < b;
          \<forall>x. a \<le> x & x \<le> b --> isCont f x;
          \<forall>x. a < x & x < b --> DERIV f x :> 0 |]
-        ==> (f b = f a)"
+        ==> f b = f a"
 apply (drule MVT, assumption)
 apply (blast intro: differentiableI)
 apply (auto dest!: DERIV_unique simp add: diff_eq_eq)
@@ -1992,7 +1981,7 @@
   assumes d: "0 < d"
       and inj: "\<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z"
       and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z"
-  shows "\<exists>e. 0<e & (\<forall>y. \<bar>y - f x\<bar> \<le> e --> (\<exists>z. \<bar>z-x\<bar> \<le> d & f z = y))"
+  shows "\<exists>e>0. \<forall>y. \<bar>y - f x\<bar> \<le> e --> (\<exists>z. \<bar>z-x\<bar> \<le> d & f z = y)"
 proof -
   have "x-d \<le> x+d" "\<forall>z. x-d \<le> z \<and> z \<le> x+d \<longrightarrow> isCont f z" using cont d
     by (auto simp add: abs_le_interval_iff)
@@ -2045,7 +2034,7 @@
   shows "isCont g (f x)"
 proof (simp add: isCont_iff LIM_eq)
   show "\<forall>r. 0 < r \<longrightarrow>
-         (\<exists>s. 0<s \<and> (\<forall>z. z\<noteq>0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>g(f x + z) - g(f x)\<bar> < r))"
+         (\<exists>s>0. \<forall>z. z\<noteq>0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>g(f x + z) - g(f x)\<bar> < r)"
   proof (intro strip)
     fix r::real
     assume r: "0<r"
@@ -2058,7 +2047,7 @@
     obtain e' where e': "0 < e'"
         and all: "\<forall>y. \<bar>y - f x\<bar> \<le> e' \<longrightarrow> (\<exists>z. \<bar>z - x\<bar> \<le> e \<and> f z = y)"
           by blast
-    show "\<exists>s. 0<s \<and> (\<forall>z. z\<noteq>0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>g(f x + z) - g(f x)\<bar> < r)"
+    show "\<exists>s>0. \<forall>z. z\<noteq>0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>g(f x + z) - g(f x)\<bar> < r"
     proof (intro exI conjI)
       show "0<e'" .
       show "\<forall>z. z \<noteq> 0 \<and> \<bar>z\<bar> < e' \<longrightarrow> \<bar>g (f x + z) - g (f x)\<bar> < r"
@@ -2269,4 +2258,3 @@
 
 
 end
-
diff -r 8bad1f42fec0 -r 300e09825d8b src/HOL/Hyperreal/NatStar.thy
--- a/src/HOL/Hyperreal/NatStar.thy	Thu Dec 02 11:09:19 2004 +0100
+++ b/src/HOL/Hyperreal/NatStar.thy	Thu Dec 02 11:42:01 2004 +0100
@@ -8,7 +8,7 @@
 header{*Star-transforms for the Hypernaturals*}
 
 theory NatStar
-imports "../Real/RealPow" HyperPow
+imports HyperPow
 begin
 
 text{*Extends sets of nats, and functions from the nats to nats or reals*}
@@ -638,5 +638,3 @@
 
 
 end
-
-
diff -r 8bad1f42fec0 -r 300e09825d8b src/HOL/Hyperreal/SEQ.thy
--- a/src/HOL/Hyperreal/SEQ.thy	Thu Dec 02 11:09:19 2004 +0100
+++ b/src/HOL/Hyperreal/SEQ.thy	Thu Dec 02 11:42:01 2004 +0100
@@ -37,7 +37,7 @@
 
   Bseq :: "(nat => real) => bool"
     --{*Standard definition for bounded sequence*}
-  "Bseq X == (\<exists>K. (0 < K & (\<forall>n. \<bar>X n\<bar> \<le> K)))"
+  "Bseq X == \<exists>K>0.\<forall>n. \<bar>X n\<bar> \<le> K"
 
   NSBseq :: "(nat=>real) => bool"
     --{*Nonstandard definition for bounded sequence*}
@@ -45,18 +45,15 @@
 
   monoseq :: "(nat=>real)=>bool"
     --{*Definition for monotonicity*}
-  "monoseq X == ((\<forall>(m::nat) n. m \<le> n --> X m \<le> X n) |
-                 (\<forall>m n. m \<le> n --> X n \<le> X m))"
+  "monoseq X == (\<forall>m. \<forall>n\<ge>m. X m \<le> X n) | (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)"
 
   subseq :: "(nat => nat) => bool"
     --{*Definition of subsequence*}
-  "subseq f == (\<forall>m n. m < n --> (f m) < (f n))"
+  "subseq f == \<forall>m. \<forall>n>m. (f m) < (f n)"
 
   Cauchy :: "(nat => real) => bool"
     --{*Standard definition of the Cauchy condition*}
-  "Cauchy X == (\<forall>e. (0 < e -->
-                       (\<exists>M. (\<forall>m n. M \<le> m & M \<le> n
-                             --> abs((X m) + -(X n)) < e))))"
+  "Cauchy X == \<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. abs((X m) + -(X n)) < e"
 
   NSCauchy :: "(nat => real) => bool"
     --{*Nonstandard definition*}
@@ -80,8 +77,7 @@
 subsection{*LIMSEQ and NSLIMSEQ*}
 
 lemma LIMSEQ_iff:
-      "(X ----> L) =
-       (\<forall>r. 0 <r --> (\<exists>no. \<forall>n. no \<le> n --> \<bar>X n + -L\<bar> < r))"
+      "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. \<bar>X n + -L\<bar> < r)"
 by (simp add: LIMSEQ_def)
 
 lemma NSLIMSEQ_iff:
@@ -363,10 +359,10 @@
 apply (auto intro: order_trans)
 done
 
-lemma monoI1: "\<forall>m n. m \<le> n --> X m \<le> X n ==> monoseq X"
+lemma monoI1: "\<forall>m. \<forall> n \<ge> m. X m \<le> X n ==> monoseq X"
 by (simp add: monoseq_def)
 
-lemma monoI2: "\<forall>m n. m \<le> n --> X n \<le> X m ==> monoseq X"
+lemma monoI2: "\<forall>m. \<forall> n \<ge> m. X n \<le> X m ==> monoseq X"
 by (simp add: monoseq_def)
 
 lemma mono_SucI1: "\<forall>n. X n \<le> X (Suc n) ==> monoseq X"
@@ -385,7 +381,7 @@
 by (auto simp add: Bseq_def)
 
 lemma lemma_NBseq_def:
-     "(\<exists>K. 0 < K & (\<forall>n. \<bar>X n\<bar> \<le> K)) =
+     "(\<exists>K > 0. \<forall>n. \<bar>X n\<bar> \<le> K) =
       (\<exists>N. \<forall>n. \<bar>X n\<bar> \<le> real(Suc N))"
 apply auto
  prefer 2 apply force
@@ -402,8 +398,7 @@
 done
 
 lemma lemma_NBseq_def2:
-     "(\<exists>K. 0 < K & (\<forall>n. \<bar>X n\<bar> \<le> K)) =
-      (\<exists>N. \<forall>n. \<bar>X n\<bar> < real(Suc N))"
+     "(\<exists>K > 0. \<forall>n. \<bar>X n\<bar> \<le> K) = (\<exists>N. \<forall>n. \<bar>X n\<bar> < real(Suc N))"
 apply (subst lemma_NBseq_def, auto)
 apply (rule_tac x = "Suc N" in exI)
 apply (rule_tac [2] x = N in exI)
@@ -449,13 +444,13 @@
    which woulid be useless.*}
 
 lemma lemmaNSBseq:
-     "\<forall>K. 0 < K --> (\<exists>n. K < \<bar>X n\<bar>)
+     "\<forall>K > 0. \<exists>n. K < \<bar>X n\<bar>
       ==> \<forall>N. \<exists>n. real(Suc N) < \<bar>X n\<bar>"
 apply safe
 apply (cut_tac n = N in real_of_nat_Suc_gt_zero, blast)
 done
 
-lemma lemmaNSBseq2: "\<forall>K. 0 < K --> (\<exists>n. K < \<bar>X n\<bar>)
+lemma lemmaNSBseq2: "\<forall>K > 0. \<exists>n. K < \<bar>X n\<bar>
                      ==> \<exists>f. \<forall>N. real(Suc N) < \<bar>X (f N)\<bar>"
 apply (drule lemmaNSBseq)
 apply (drule choice, blast)
@@ -558,9 +553,9 @@
 subsection{*A Bounded and Monotonic Sequence Converges*}
 
 lemma lemma_converg1:
-     "!!(X::nat=>real). [| \<forall>m n. m \<le> n -->  X m \<le> X n;
+     "!!(X::nat=>real). [| \<forall>m. \<forall> n \<ge> m. X m \<le> X n;
                   isLub (UNIV::real set) {x. \<exists>n. X n = x} (X ma)
-               |] ==> \<forall>n. ma \<le> n --> X n = X ma"
+               |] ==> \<forall>n \<ge> ma. X n = X ma"
 apply safe
 apply (drule_tac y = "X n" in isLubD2)
 apply (blast dest: order_antisym)+
@@ -578,7 +573,7 @@
 done
 
 text{*Now, the same theorem in terms of NS limit *}
-lemma Bmonoseq_NSLIMSEQ: "\<forall>n. m \<le> n --> X n = X m ==> \<exists>L. (X ----NS> L)"
+lemma Bmonoseq_NSLIMSEQ: "\<forall>n \<ge> m. X n = X m ==> \<exists>L. (X ----NS> L)"
 by (auto dest!: Bmonoseq_LIMSEQ simp add: LIMSEQ_NSLIMSEQ_iff)
 
 lemma lemma_converg2:
@@ -610,7 +605,7 @@
 text{*A standard proof of the theorem for monotone increasing sequence*}
 
 lemma Bseq_mono_convergent:
-     "[| Bseq X; \<forall>m n. m \<le> n --> X m \<le> X n |] ==> convergent X"
+     "[| Bseq X; \<forall>m. \<forall>n \<ge> m. X m \<le> X n |] ==> convergent X"
 apply (simp add: convergent_def)
 apply (frule Bseq_isLub, safe)
 apply (case_tac "\<exists>m. X m = U", auto)
@@ -629,7 +624,7 @@
 text{*Nonstandard version of the theorem*}
 
 lemma NSBseq_mono_NSconvergent:
-     "[| NSBseq X; \<forall>m n. m \<le> n --> X m \<le> X n |] ==> NSconvergent X"
+     "[| NSBseq X; \<forall>m. \<forall>n \<ge> m. X m \<le> X n |] ==> NSconvergent X"
 by (auto intro: Bseq_mono_convergent 
          simp add: convergent_NSconvergent_iff [symmetric] 
                    Bseq_NSBseq_iff [symmetric])
@@ -655,16 +650,16 @@
 subsection{*A Few More Equivalence Theorems for Boundedness*}
 
 text{*alternative formulation for boundedness*}
-lemma Bseq_iff2: "Bseq X = (\<exists>k x. 0 < k & (\<forall>n. \<bar>X(n) + -x\<bar> \<le> k))"
+lemma Bseq_iff2: "Bseq X = (\<exists>k > 0. \<exists>x. \<forall>n. \<bar>X(n) + -x\<bar> \<le> k)"
 apply (unfold Bseq_def, safe)
 apply (rule_tac [2] x = "k + \<bar>x\<bar> " in exI)
-apply (rule_tac x = K in exI)
+apply (rule_tac x = K in exI, simp)
 apply (rule exI [where x = 0], auto)
 apply (drule_tac x=n in spec, arith)+
 done
 
 text{*alternative formulation for boundedness*}
-lemma Bseq_iff3: "Bseq X = (\<exists>k N. 0 < k & (\<forall>n. abs(X(n) + -X(N)) \<le> k))"
+lemma Bseq_iff3: "Bseq X = (\<exists>k > 0. \<exists>N. \<forall>n. abs(X(n) + -X(N)) \<le> k)"
 apply safe
 apply (simp add: Bseq_def, safe)
 apply (rule_tac x = "K + \<bar>X N\<bar> " in exI)
@@ -746,8 +741,8 @@
 text{*A Cauchy sequence is bounded -- this is the standard
   proof mechanization rather than the nonstandard proof*}
 
-lemma lemmaCauchy: "\<forall>n. M \<le> n --> \<bar>X M + - X n\<bar> < (1::real)
-          ==>  \<forall>n. M \<le> n --> \<bar>X n\<bar> < 1 + \<bar>X M\<bar>"
+lemma lemmaCauchy: "\<forall>n \<ge> M. \<bar>X M + - X n\<bar> < (1::real)
+          ==>  \<forall>n \<ge> M. \<bar>X n\<bar> < 1 + \<bar>X M\<bar>"
 apply safe
 apply (drule spec, auto, arith)
 done
@@ -757,7 +752,7 @@
 
 text{* FIXME: Long. Maximal element in subsequence *}
 lemma SUP_rabs_subseq:
-     "\<exists>m. m \<le> M & (\<forall>n. n \<le> M --> \<bar>(X::nat=> real) n\<bar> \<le> \<bar>X m\<bar>)"
+     "\<exists>m \<le> M. \<forall>n \<le> M. \<bar>(X::nat=> real) n\<bar> \<le> \<bar>X m\<bar>"
 apply (induct M)
 apply (rule_tac x = 0 in exI, simp, safe)
 apply (cut_tac x = "\<bar>X (Suc M)\<bar>" and y = "\<bar>X m\<bar> " in linorder_less_linear)
@@ -772,28 +767,28 @@
 
 lemma lemma_Nat_covered:
      "[| \<forall>m::nat. m \<le> M --> P M m;
-         \<forall>m. M \<le> m --> P M m |]
+         \<forall>m \<ge> M. P M m |]
       ==> \<forall>m. P M m"
 by (auto elim: less_asym simp add: le_def)
 
 
 lemma lemma_trans1:
-     "[| \<forall>n. n \<le> M --> \<bar>(X::nat=>real) n\<bar> \<le> a;  a < b |]
-      ==> \<forall>n. n \<le> M --> \<bar>X n\<bar> \<le> b"
+     "[| \<forall>n \<le> M. \<bar>(X::nat=>real) n\<bar> \<le> a;  a < b |]
+      ==> \<forall>n \<le> M. \<bar>X n\<bar> \<le> b"
 by (blast intro: order_le_less_trans [THEN order_less_imp_le])
 
 lemma lemma_trans2:
-     "[| \<forall>n. M \<le> n --> \<bar>(X::nat=>real) n\<bar> < a; a < b |]
-      ==> \<forall>n. M \<le> n --> \<bar>X n\<bar>\<le> b"
+     "[| \<forall>n \<ge> M. \<bar>(X::nat=>real) n\<bar> < a; a < b |]
+      ==> \<forall>n \<ge> M. \<bar>X n\<bar>\<le> b"
 by (blast intro: order_less_trans [THEN order_less_imp_le])
 
 lemma lemma_trans3:
-     "[| \<forall>n. n \<le> M --> \<bar>X n\<bar> \<le> a; a = b |]
-      ==> \<forall>n. n \<le> M --> \<bar>X n\<bar> \<le> b"
+     "[| \<forall>n \<le> M. \<bar>X n\<bar> \<le> a; a = b |]
+      ==> \<forall>n \<le> M. \<bar>X n\<bar> \<le> b"
 by auto
 
-lemma lemma_trans4: "\<forall>n. M \<le> n --> \<bar>(X::nat=>real) n\<bar> < a
-              ==>  \<forall>n. M \<le> n --> \<bar>X n\<bar> \<le> a"
+lemma lemma_trans4: "\<forall>n \<ge> M. \<bar>(X::nat=>real) n\<bar> < a
+              ==>  \<forall>n \<ge> M. \<bar>X n\<bar> \<le> a"
 by (blast intro: order_less_imp_le)
 
 
@@ -857,8 +852,8 @@
 
 lemma NSLIMSEQ_le:
        "[| f ----NS> l; g ----NS> m;
-           \<exists>N. \<forall>n. N \<le> n --> f(n) \<le> g(n)
-                |] ==> l \<le> m"
+           \<exists>N. \<forall>n \<ge> N. f(n) \<le> g(n)
+        |] ==> l \<le> m"
 apply (simp add: NSLIMSEQ_def, safe)
 apply (drule starfun_le_mono)
 apply (drule HNatInfinite_whn [THEN [2] bspec])+
@@ -870,7 +865,7 @@
 
 (* standard version *)
 lemma LIMSEQ_le:
-     "[| f ----> l; g ----> m; \<exists>N. \<forall>n. N \<le> n --> f(n) \<le> g(n) |]
+     "[| f ----> l; g ----> m; \<exists>N. \<forall>n \<ge> N. f(n) \<le> g(n) |]
       ==> l \<le> m"
 by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_le)
 
@@ -952,7 +947,7 @@
 
 text{* standard proof seems easier *}
 lemma LIMSEQ_inverse_zero:
-      "\<forall>y. \<exists>N. \<forall>n. N \<le> n --> y < f(n) ==> (%n. inverse(f n)) ----> 0"
+      "\<forall>y. \<exists>N. \<forall>n \<ge> N. y < f(n) ==> (%n. inverse(f n)) ----> 0"
 apply (simp add: LIMSEQ_def, safe)
 apply (drule_tac x = "inverse r" in spec, safe)
 apply (rule_tac x = N in exI, safe)
@@ -967,7 +962,7 @@
 done
 
 lemma NSLIMSEQ_inverse_zero:
-     "\<forall>y. \<exists>N. \<forall>n. N \<le> n --> y < f(n)
+     "\<forall>y. \<exists>N. \<forall>n \<ge> N. y < f(n)
       ==> (%n. inverse(f n)) ----NS> 0"
 by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_zero)
 
@@ -1240,4 +1235,3 @@
 
 
 end
-
diff -r 8bad1f42fec0 -r 300e09825d8b src/HOL/Hyperreal/Series.thy
--- a/src/HOL/Hyperreal/Series.thy	Thu Dec 02 11:09:19 2004 +0100
+++ b/src/HOL/Hyperreal/Series.thy	Thu Dec 02 11:42:01 2004 +0100
@@ -84,7 +84,7 @@
 done
 
 lemma sumr_interval_const2:
-     "[|\<forall>n. m \<le> n --> f n = r; m \<le> k|]
+     "[|\<forall>n\<ge>m. f n = r; m \<le> k|]
       ==> sumr m k f = (real (k - m) * r)"
 apply (induct "k", auto) 
 apply (drule_tac x = k in spec)
@@ -94,7 +94,7 @@
 
 
 lemma sumr_le:
-     "[|\<forall>n. m \<le> n --> 0 \<le> f n; m < k|] ==> sumr 0 m f \<le> sumr 0 k f"
+     "[|\<forall>n\<ge>m. 0 \<le> f n; m < k|] ==> sumr 0 m f \<le> sumr 0 k f"
 apply (induct "k")
 apply (auto simp add: less_Suc_eq_le)
 apply (drule_tac x = k in spec, safe)
@@ -109,7 +109,7 @@
 apply (auto intro: add_mono simp add: le_def)
 done
 
-lemma sumr_ge_zero: "(\<forall>n. m \<le> n --> 0 \<le> f n) --> 0 \<le> sumr m n f"
+lemma sumr_ge_zero: "(\<forall>n\<ge>m. 0 \<le> f n) --> 0 \<le> sumr m n f"
 apply (induct "n", auto)
 apply (drule_tac x = n in spec, arith)
 done
@@ -119,11 +119,11 @@
 by (induct "n", simp_all add: add_increasing)
 
 lemma sumr_zero [rule_format]:
-     "\<forall>n. N \<le> n --> f n = 0 ==> N \<le> m --> sumr m n f = 0"
+     "\<forall>n \<ge> N. f n = 0 ==> N \<le> m --> sumr m n f = 0"
 by (induct "n", auto)
 
 lemma Suc_le_imp_diff_ge2:
-     "[|\<forall>n. N \<le> n --> f (Suc n) = 0; Suc N \<le> m|] ==> sumr m n f = 0"
+     "[|\<forall>n \<ge> N. f (Suc n) = 0; Suc N \<le> m|] ==> sumr m n f = 0"
 apply (rule sumr_zero) 
 apply (case_tac "n", auto)
 done
@@ -289,7 +289,7 @@
 great as any partial sum.*}
 
 lemma series_pos_le: 
-     "[| summable f; \<forall>m. n \<le> m --> 0 \<le> f(m) |] ==> sumr 0 n f \<le> suminf f"
+     "[| summable f; \<forall>m \<ge> n. 0 \<le> f(m) |] ==> sumr 0 n f \<le> suminf f"
 apply (drule summable_sums)
 apply (simp add: sums_def)
 apply (cut_tac k = "sumr 0 n f" in LIMSEQ_const)
@@ -300,7 +300,7 @@
 done
 
 lemma series_pos_less:
-     "[| summable f; \<forall>m. n \<le> m --> 0 < f(m) |] ==> sumr 0 n f < suminf f"
+     "[| summable f; \<forall>m \<ge> n. 0 < f(m) |] ==> sumr 0 n f < suminf f"
 apply (rule_tac y = "sumr 0 (Suc n) f" in order_less_le_trans)
 apply (rule_tac [2] series_pos_le, auto)
 apply (drule_tac x = m in spec, auto)
@@ -332,14 +332,14 @@
 
 lemma summable_Cauchy:
      "summable f =  
-      (\<forall>e. 0 < e --> (\<exists>N. \<forall>m n. N \<le> m --> abs(sumr m n f) < e))"
+      (\<forall>e > 0. \<exists>N. \<forall>m \<ge> N. \<forall>n. abs(sumr m n f) < e)"
 apply (auto simp add: summable_convergent_sumr_iff Cauchy_convergent_iff [symmetric] Cauchy_def)
 apply (drule_tac [!] spec, auto) 
 apply (rule_tac x = M in exI)
 apply (rule_tac [2] x = N in exI, auto)
 apply (cut_tac [!] m = m and n = n in less_linear, auto)
 apply (frule le_less_trans [THEN less_imp_le], assumption)
-apply (drule_tac x = n in spec)
+apply (drule_tac x = n in spec, simp)
 apply (drule_tac x = m in spec)
 apply (auto intro: abs_minus_add_cancel [THEN subst]
             simp add: sumr_split_add_minus abs_minus_add_cancel)
@@ -348,7 +348,7 @@
 text{*Comparison test*}
 
 lemma summable_comparison_test:
-     "[| \<exists>N. \<forall>n. N \<le> n --> abs(f n) \<le> g n; summable g |] ==> summable f"
+     "[| \<exists>N. \<forall>n \<ge> N. abs(f n) \<le> g n; summable g |] ==> summable f"
 apply (auto simp add: summable_Cauchy)
 apply (drule spec, auto)
 apply (rule_tac x = "N + Na" in exI, auto)
@@ -362,7 +362,7 @@
 done
 
 lemma summable_rabs_comparison_test:
-     "[| \<exists>N. \<forall>n. N \<le> n --> abs(f n) \<le> g n; summable g |] 
+     "[| \<exists>N. \<forall>n \<ge> N. abs(f n) \<le> g n; summable g |] 
       ==> summable (%k. abs (f k))"
 apply (rule summable_comparison_test)
 apply (auto simp add: abs_idempotent)
@@ -419,7 +419,7 @@
 
 (*All this trouble just to get 0<c *)
 lemma ratio_test_lemma2:
-     "[| \<forall>n. N \<le> n --> abs(f(Suc n)) \<le> c*abs(f n) |]  
+     "[| \<forall>n \<ge> N. abs(f(Suc n)) \<le> c*abs(f n) |]  
       ==> 0 < c | summable f"
 apply (simp (no_asm) add: linorder_not_le [symmetric])
 apply (simp add: summable_Cauchy)
@@ -430,7 +430,7 @@
 done
 
 lemma ratio_test:
-     "[| c < 1; \<forall>n. N \<le> n --> abs(f(Suc n)) \<le> c*abs(f n) |]  
+     "[| c < 1; \<forall>n \<ge> N. abs(f(Suc n)) \<le> c*abs(f n) |]  
       ==> summable f"
 apply (frule ratio_test_lemma2, auto)
 apply (rule_tac g = "%n. (abs (f N) / (c ^ N))*c ^ n"