# HG changeset patch
# User paulson
# Date 993567910 -7200
# Node ID 297625089e80a60498867d6f74e25726bde3ecee
# Parent  a816fead971a8e5ff03a2f2b12576073191d21e5
tidied

diff -r a816fead971a -r 297625089e80 src/HOL/Divides.ML
--- a/src/HOL/Divides.ML	Tue Jun 26 17:04:54 2001 +0200
+++ b/src/HOL/Divides.ML	Tue Jun 26 17:05:10 2001 +0200
@@ -592,15 +592,10 @@
 by (rtac dvd_refl 1);
 qed "dvd_reduce";
 
-Goalw [dvd_def] "!!n::nat. [| f dvd m; f dvd n; 0<n |] ==> f dvd m mod n";
-by (Clarify_tac 1);
-by (Full_simp_tac 1);
-by (res_inst_tac 
-    [("x", "(((k div ka)*ka + k mod ka) - ((f*k) div (f*ka)) * ka)")] 
-    exI 1);
-by (asm_simp_tac
-    (simpset() addsimps [diff_mult_distrib2, mod_mult_distrib2 RS sym, 
-			 add_mult_distrib2]) 1);
+Goalw [dvd_def] "!!n::nat. [| f dvd m; f dvd n |] ==> f dvd m mod n";
+by (div_undefined_case_tac "n=0" 1);
+by Auto_tac; 
+by (blast_tac (claset() addIs [mod_mult_distrib2 RS sym]) 1);  
 qed "dvd_mod";
 
 Goal "[| (k::nat) dvd m mod n;  k dvd n |] ==> k dvd m";
@@ -609,19 +604,6 @@
 by (asm_full_simp_tac (simpset() addsimps [mod_div_equality]) 1);
 qed "dvd_mod_imp_dvd";
 
-Goalw [dvd_def] "!!n::nat. [| f dvd m; f dvd n |] ==> f dvd m mod n";
-by (div_undefined_case_tac "n=0" 1);
-by (Clarify_tac 1);
-by (Full_simp_tac 1);
-by (rename_tac "j" 1);
-by (res_inst_tac 
-    [("x", "(((k div j)*j + k mod j) - ((f*k) div (f*j)) * j)")] 
-    exI 1);
-by (asm_simp_tac
-    (simpset() addsimps [diff_mult_distrib2, mod_mult_distrib2 RS sym, 
-			 add_mult_distrib2]) 1);
-qed "dvd_mod";
-
 Goal "k dvd n ==> ((k::nat) dvd m mod n) = (k dvd m)";
 by (blast_tac (claset() addIs [dvd_mod_imp_dvd, dvd_mod]) 1); 
 qed "dvd_mod_iff";
diff -r a816fead971a -r 297625089e80 src/HOL/Hyperreal/Lim.ML
--- a/src/HOL/Hyperreal/Lim.ML	Tue Jun 26 17:04:54 2001 +0200
+++ b/src/HOL/Hyperreal/Lim.ML	Tue Jun 26 17:05:10 2001 +0200
@@ -73,7 +73,7 @@
 (*--------------------------
    Limit not zero
  --------------------------*)
-Goalw [LIM_def] "k ~= #0 ==> ~ ((%x. k) -- x --> #0)";
+Goalw [LIM_def] "k \\<noteq> #0 ==> ~ ((%x. k) -- x --> #0)";
 by (res_inst_tac [("R1.0","k"),("R2.0","#0")] real_linear_less2 1);
 by (auto_tac (claset(), simpset() addsimps [real_abs_def]));
 by (res_inst_tac [("x","-k")] exI 1);
@@ -85,7 +85,7 @@
 by Auto_tac;  
 qed "LIM_not_zero";
 
-(* [| k ~= #0; (%x. k) -- x --> #0 |] ==> R *)
+(* [| k \\<noteq> #0; (%x. k) -- x --> #0 |] ==> R *)
 bind_thm("LIM_not_zeroE", LIM_not_zero RS notE);
 
 Goal "(%x. k) -- x --> L ==> k = L";
@@ -107,8 +107,8 @@
 (*-------------
     LIM_mult_zero
  -------------*)
-Goalw [LIM_def] "[| f -- x --> #0; g -- x --> #0 |] \
-\         ==> (%x. f(x)*g(x)) -- x --> #0";
+Goalw [LIM_def]
+     "[| f -- x --> #0; g -- x --> #0 |] ==> (%x. f(x)*g(x)) -- x --> #0";
 by Safe_tac;
 by (dres_inst_tac [("x","#1")] spec 1);
 by (dres_inst_tac [("x","r")] spec 1);
@@ -141,14 +141,13 @@
    Limits are equal for functions equal except at limit point
  --------------------------------------------------------------*)
 Goalw [LIM_def] 
-      "[| ALL x. x ~= a --> (f x = g x) |] \
-\           ==> (f -- a --> l) = (g -- a --> l)";
+     "[| \\<forall>x. x \\<noteq> a --> (f x = g x) |] \
+\     ==> (f -- a --> l) = (g -- a --> l)";
 by (auto_tac (claset(), simpset() addsimps [real_add_minus_iff]));
 qed "LIM_equal";
 
-Goal "[| (%x. f(x) + -g(x)) -- a --> #0; \
-\        g -- a --> l |] \
-\      ==> f -- a --> l";
+Goal "[| (%x. f(x) + -g(x)) -- a --> #0;  g -- a --> l |] \
+\     ==> f -- a --> l";
 by (dtac LIM_add 1 THEN assume_tac 1);
 by (auto_tac (claset(), simpset() addsimps [real_add_assoc]));
 qed "LIM_trans";
@@ -171,7 +170,7 @@
 by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2 THEN Step_tac 1);
 by (dres_inst_tac [("x","u")] spec 1 THEN Clarify_tac 1);
 by (dres_inst_tac [("x","s")] spec 1 THEN Clarify_tac 1);
-by (subgoal_tac "ALL n::nat. (xa n) ~= x & \
+by (subgoal_tac "\\<forall>n::nat. (xa n) \\<noteq> x & \
 \                    abs ((xa n) + - x) < s --> abs (f (xa n) + - L) < u" 1);
 by (Blast_tac 2);
 by (dtac FreeUltrafilterNat_all 1);
@@ -182,29 +181,29 @@
     Limit: NS definition ==> standard definition
  ---------------------------------------------------------------------*)
 
-Goal "ALL s. #0 < s --> (EX xa.  xa ~= x & \
-\        abs (xa + - x) < s  & r <= abs (f xa + -L)) \
-\     ==> ALL n::nat. EX xa.  xa ~= x & \
-\             abs(xa + -x) < inverse(real(Suc n)) & r <= abs(f xa + -L)";
+Goal "\\<forall>s. #0 < s --> (\\<exists>xa.  xa \\<noteq> x & \
+\        abs (xa + - x) < s  & r \\<le> abs (f xa + -L)) \
+\     ==> \\<forall>n::nat. \\<exists>xa.  xa \\<noteq> x & \
+\             abs(xa + -x) < inverse(real(Suc n)) & r \\<le> abs(f xa + -L)";
 by (Clarify_tac 1); 
 by (cut_inst_tac [("n1","n")]
     (real_of_nat_Suc_gt_zero RS rename_numerals real_inverse_gt_zero) 1);
 by Auto_tac;
 val lemma_LIM = result();
 
-Goal "ALL s. #0 < s --> (EX xa.  xa ~= x & \
-\        abs (xa + - x) < s  & r <= abs (f xa + -L)) \
-\     ==> EX X. ALL n::nat. X n ~= x & \
-\               abs(X n + -x) < inverse(real(Suc n)) & r <= abs(f (X n) + -L)";
+Goal "\\<forall>s. #0 < s --> (\\<exists>xa.  xa \\<noteq> x & \
+\        abs (xa + - x) < s  & r \\<le> abs (f xa + -L)) \
+\     ==> \\<exists>X. \\<forall>n::nat. X n \\<noteq> x & \
+\               abs(X n + -x) < inverse(real(Suc n)) & r \\<le> abs(f (X n) + -L)";
 by (dtac lemma_LIM 1);
 by (dtac choice 1);
 by (Blast_tac 1);
 val lemma_skolemize_LIM2 = result();
 
-Goal "ALL n. X n ~= x & \
+Goal "\\<forall>n. X n \\<noteq> x & \
 \         abs (X n + - x) < inverse (real(Suc n)) & \
-\         r <= abs (f (X n) + - L) ==> \
-\         ALL n. abs (X n + - x) < inverse (real(Suc n))";
+\         r \\<le> abs (f (X n) + - L) ==> \
+\         \\<forall>n. abs (X n + - x) < inverse (real(Suc n))";
 by (Auto_tac );
 val lemma_simp = result();
  
@@ -321,7 +320,7 @@
     NSLIM_inverse
  -----------------------------*)
 Goalw [NSLIM_def] 
-     "[| f -- a --NS> L;  L ~= #0 |] \
+     "[| f -- a --NS> L;  L \\<noteq> #0 |] \
 \     ==> (%x. inverse(f(x))) -- a --NS> (inverse L)";
 by (Clarify_tac 1);
 by (dtac spec 1);
@@ -330,7 +329,7 @@
 qed "NSLIM_inverse";
 
 Goal "[| f -- a --> L; \
-\        L ~= #0 |] ==> (%x. inverse(f(x))) -- a --> (inverse L)";
+\        L \\<noteq> #0 |] ==> (%x. inverse(f(x))) -- a --> (inverse L)";
 by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, NSLIM_inverse]) 1);
 qed "LIM_inverse";
 
@@ -360,17 +359,17 @@
 (*--------------------------
    NSLIM_not_zero
  --------------------------*)
-Goalw [NSLIM_def] "k ~= #0 ==> ~ ((%x. k) -- x --NS> #0)";
+Goalw [NSLIM_def] "k \\<noteq> #0 ==> ~ ((%x. k) -- x --NS> #0)";
 by Auto_tac;
 by (res_inst_tac [("x","hypreal_of_real x + epsilon")] exI 1);
 by (auto_tac (claset() addIs [Infinitesimal_add_approx_self RS approx_sym],
               simpset() addsimps [rename_numerals hypreal_epsilon_not_zero]));
 qed "NSLIM_not_zero";
 
-(* [| k ~= #0; (%x. k) -- x --NS> #0 |] ==> R *)
+(* [| k \\<noteq> #0; (%x. k) -- x --NS> #0 |] ==> R *)
 bind_thm("NSLIM_not_zeroE", NSLIM_not_zero RS notE);
 
-Goal "k ~= #0 ==> ~ ((%x. k) -- x --> #0)";
+Goal "k \\<noteq> #0 ==> ~ ((%x. k) -- x --> #0)";
 by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, NSLIM_not_zero]) 1);
 qed "LIM_not_zero2";
 
@@ -438,8 +437,8 @@
  ---------------*)
 
 Goalw [isNSCont_def] 
-      "[| isNSCont f a; y @= hypreal_of_real a |] \
-\           ==> (*f* f) y @= hypreal_of_real (f a)";
+      "[| isNSCont f a; y \\<approx> hypreal_of_real a |] \
+\           ==> (*f* f) y \\<approx> hypreal_of_real (f a)";
 by (Blast_tac 1);
 qed "isNSContD";
 
@@ -575,11 +574,11 @@
 qed "isCont_minus";
 
 Goalw [isCont_def]  
-      "[| isCont f x; f x ~= #0 |] ==> isCont (%x. inverse (f x)) x";
+      "[| isCont f x; f x \\<noteq> #0 |] ==> isCont (%x. inverse (f x)) x";
 by (blast_tac (claset() addIs [LIM_inverse]) 1);
 qed "isCont_inverse";
 
-Goal "[| isNSCont f x; f x ~= #0 |] ==> isNSCont (%x. inverse (f x)) x";
+Goal "[| isNSCont f x; f x \\<noteq> #0 |] ==> isNSCont (%x. inverse (f x)) x";
 by (auto_tac (claset() addIs [isCont_inverse],simpset() addsimps 
     [isNSCont_isCont_iff]));
 qed "isNSCont_inverse";
@@ -616,11 +615,11 @@
 (%*------------------------------------------------------------
   Elementary topology proof for a characterisation of 
   continuity now: a function f is continuous if and only 
-  if the inverse image, {x. f(x) : A}, of any open set A 
+  if the inverse image, {x. f(x) \\<in> A}, of any open set A 
   is always an open set
  ------------------------------------------------------------*%)
-Goal "[| isNSopen A; ALL x. isNSCont f x |] \
-\              ==> isNSopen {x. f x : A}";
+Goal "[| isNSopen A; \\<forall>x. isNSCont f x |] \
+\              ==> isNSopen {x. f x \\<in> A}";
 by (auto_tac (claset(),simpset() addsimps [isNSopen_iff1]));
 by (dtac (mem_monad_approx RS approx_sym) 1);
 by (dres_inst_tac [("x","a")] spec 1);
@@ -631,7 +630,7 @@
 qed "isNSCont_isNSopen";
 
 Goalw [isNSCont_def]
-          "ALL A. isNSopen A --> isNSopen {x. f x : A} \
+          "\\<forall>A. isNSopen A --> isNSopen {x. f x \\<in> A} \
 \              ==> isNSCont f x";
 by (auto_tac (claset() addSIs [(mem_infmal_iff RS iffD1) RS 
      (approx_minus_iff RS iffD2)],simpset() addsimps 
@@ -644,15 +643,15 @@
     simpset() addsimps [hypreal_of_real_zero RS sym,STAR_starfun_rabs_add_minus]));
 qed "isNSopen_isNSCont";
 
-Goal "(ALL x. isNSCont f x) = \
-\     (ALL A. isNSopen A --> isNSopen {x. f(x) : A})";
+Goal "(\\<forall>x. isNSCont f x) = \
+\     (\\<forall>A. isNSopen A --> isNSopen {x. f(x) \\<in> A})";
 by (blast_tac (claset() addIs [isNSCont_isNSopen,
     isNSopen_isNSCont]) 1);
 qed "isNSCont_isNSopen_iff";
 
 (%*------- Standard version of same theorem --------*%)
-Goal "(ALL x. isCont f x) = \
-\         (ALL A. isopen A --> isopen {x. f(x) : A})";
+Goal "(\\<forall>x. isCont f x) = \
+\         (\\<forall>A. isopen A --> isopen {x. f(x) \\<in> A})";
 by (auto_tac (claset() addSIs [isNSCont_isNSopen_iff],
               simpset() addsimps [isNSopen_isopen_iff RS sym,
               isNSCont_isCont_iff RS sym]));
@@ -663,12 +662,12 @@
                         Uniform continuity
  ------------------------------------------------------------------*)
 Goalw [isNSUCont_def] 
-      "[| isNSUCont f; x @= y|] ==> (*f* f) x @= (*f* f) y";
+      "[| isNSUCont f; x \\<approx> y|] ==> (*f* f) x \\<approx> (*f* f) y";
 by (Blast_tac 1);
 qed "isNSUContD";
 
 Goalw [isUCont_def,isCont_def,LIM_def]
-     "isUCont f ==> EX x. isCont f x";
+     "isUCont f ==> \\<exists>x. isCont f x";
 by (Force_tac 1);
 qed "isUCont_isCont";
 
@@ -684,27 +683,27 @@
 by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2 THEN Step_tac 1);
 by (dres_inst_tac [("x","u")] spec 1 THEN Clarify_tac 1);
 by (dres_inst_tac [("x","s")] spec 1 THEN Clarify_tac 1);
-by (subgoal_tac "ALL n::nat. abs ((xa n) + - (xb n)) < s --> abs (f (xa n) + - f (xb n)) < u" 1);
+by (subgoal_tac "\\<forall>n::nat. abs ((xa n) + - (xb n)) < s --> abs (f (xa n) + - f (xb n)) < u" 1);
 by (Blast_tac 2);
-by (thin_tac "ALL x y. abs (x + - y) < s --> abs (f x + - f y) < u" 1);
+by (thin_tac "\\<forall>x y. abs (x + - y) < s --> abs (f x + - f y) < u" 1);
 by (dtac FreeUltrafilterNat_all 1);
 by (Ultra_tac 1);
 qed "isUCont_isNSUCont";
 
-Goal "ALL s. #0 < s --> (EX z y. abs (z + - y) < s & r <= abs (f z + -f y)) \
-\     ==> ALL n::nat. EX z y.  \
+Goal "\\<forall>s. #0 < s --> (\\<exists>z y. abs (z + - y) < s & r \\<le> abs (f z + -f y)) \
+\     ==> \\<forall>n::nat. \\<exists>z y.  \
 \              abs(z + -y) < inverse(real(Suc n)) & \
-\              r <= abs(f z + -f y)";
+\              r \\<le> abs(f z + -f y)";
 by (Clarify_tac 1); 
 by (cut_inst_tac [("n1","n")]
     (real_of_nat_Suc_gt_zero RS rename_numerals real_inverse_gt_zero) 1);
 by Auto_tac;
 val lemma_LIMu = result();
 
-Goal "ALL s. #0 < s --> (EX z y. abs (z + - y) < s  & r <= abs (f z + -f y)) \
-\     ==> EX X Y. ALL n::nat. \
+Goal "\\<forall>s. #0 < s --> (\\<exists>z y. abs (z + - y) < s  & r \\<le> abs (f z + -f y)) \
+\     ==> \\<exists>X Y. \\<forall>n::nat. \
 \              abs(X n + -(Y n)) < inverse(real(Suc n)) & \
-\              r <= abs(f (X n) + -f (Y n))";
+\              r \\<le> abs(f (X n) + -f (Y n))";
 by (dtac lemma_LIMu 1);
 by (dtac choice 1);
 by Safe_tac;
@@ -712,9 +711,9 @@
 by (Blast_tac 1);
 val lemma_skolemize_LIM2u = result();
 
-Goal "ALL n. abs (X n + -Y n) < inverse (real(Suc n)) & \
-\         r <= abs (f (X n) + - f(Y n)) ==> \
-\         ALL n. abs (X n + - Y n) < inverse (real(Suc n))";
+Goal "\\<forall>n. abs (X n + -Y n) < inverse (real(Suc n)) & \
+\         r \\<le> abs (f (X n) + - f(Y n)) ==> \
+\         \\<forall>n. abs (X n + - Y n) < inverse (real(Suc n))";
 by (Auto_tac );
 val lemma_simpu = result();
 
@@ -786,7 +785,7 @@
  ------------------------------------------------------------------------*)
 
 Goalw [differentiable_def] 
-      "f differentiable x ==> EX D. DERIV f x :> D";
+      "f differentiable x ==> \\<exists>D. DERIV f x :> D";
 by (assume_tac 1);
 qed "differentiableD";
 
@@ -796,7 +795,7 @@
 qed "differentiableI";
 
 Goalw [NSdifferentiable_def] 
-      "f NSdifferentiable x ==> EX D. NSDERIV f x :> D";
+      "f NSdifferentiable x ==> \\<exists>D. NSDERIV f x :> D";
 by (assume_tac 1);
 qed "NSdifferentiableD";
 
@@ -856,17 +855,17 @@
 (* while we're at it! *)
 Goalw [real_diff_def]
      "(NSDERIV f x :> D) = \
-\     (ALL xa. \
-\       xa ~= hypreal_of_real x & xa @= hypreal_of_real x --> \
-\       (*f* (%z. (f z - f x) / (z - x))) xa @= hypreal_of_real D)";
+\     (\\<forall>xa. \
+\       xa \\<noteq> hypreal_of_real x & xa \\<approx> hypreal_of_real x --> \
+\       (*f* (%z. (f z - f x) / (z - x))) xa \\<approx> hypreal_of_real D)";
 by (auto_tac (claset(), simpset() addsimps [NSDERIV_NSLIM_iff2, NSLIM_def]));
 qed "NSDERIV_iff2";
 
 
 Goal "(NSDERIV f x :> D) ==> \
-\    (ALL u. \
-\       u @= hypreal_of_real x --> \
-\       (*f* (%z. f z - f x)) u @= hypreal_of_real D * (u - hypreal_of_real x))";
+\    (\\<forall>u. \
+\       u \\<approx> hypreal_of_real x --> \
+\       (*f* (%z. f z - f x)) u \\<approx> hypreal_of_real D * (u - hypreal_of_real x))";
 by (auto_tac (claset(), simpset() addsimps [NSDERIV_iff2]));
 by (case_tac "u = hypreal_of_real x" 1);
 by (auto_tac (claset(), 
@@ -876,7 +875,7 @@
 by (dres_inst_tac [("c","u - hypreal_of_real x"),("b","hypreal_of_real D")]
      approx_mult1 1);
 by (ALLGOALS(dtac (hypreal_not_eq_minus_iff RS iffD1)));
-by (subgoal_tac "(*f* (%z. z - x)) u ~= (0::hypreal)" 2);
+by (subgoal_tac "(*f* (%z. z - x)) u \\<noteq> (0::hypreal)" 2);
 by (rotate_tac ~1 2);
 by (auto_tac (claset(),
     simpset() addsimps [real_diff_def, hypreal_diff_def, 
@@ -885,9 +884,9 @@
 qed "NSDERIVD5";
 
 Goal "(NSDERIV f x :> D) ==> \
-\     (ALL h: Infinitesimal. \
+\     (\\<forall>h \\<in> Infinitesimal. \
 \              ((*f* f)(hypreal_of_real x + h) - \
-\                hypreal_of_real (f x))@= (hypreal_of_real D) * h)";
+\                hypreal_of_real (f x))\\<approx> (hypreal_of_real D) * h)";
 by (auto_tac (claset(),simpset() addsimps [nsderiv_def]));
 by (case_tac "h = (0::hypreal)" 1);
 by (auto_tac (claset(),simpset() addsimps [hypreal_diff_def]));
@@ -898,9 +897,9 @@
 qed "NSDERIVD4";
 
 Goal "(NSDERIV f x :> D) ==> \
-\     (ALL h: Infinitesimal - {0}. \
+\     (\\<forall>h \\<in> Infinitesimal - {0}. \
 \              ((*f* f)(hypreal_of_real x + h) - \
-\                hypreal_of_real (f x))@= (hypreal_of_real D) * h)";
+\                hypreal_of_real (f x))\\<approx> (hypreal_of_real D) * h)";
 by (auto_tac (claset(),simpset() addsimps [nsderiv_def]));
 by (rtac ccontr 1 THEN dres_inst_tac [("x","h")] bspec 1);
 by (dres_inst_tac [("c","h")] approx_mult1 2);
@@ -999,9 +998,9 @@
 by (simp_tac (simpset() addsimps [hypreal_add_mult_distrib2]) 1);
 val lemma_nsderiv1 = result();
 
-Goal "[| (x + y) / z = hypreal_of_real D + yb; z ~= 0; \
-\        z : Infinitesimal; yb : Infinitesimal |] \
-\     ==> x + y @= #0";
+Goal "[| (x + y) / z = hypreal_of_real D + yb; z \\<noteq> 0; \
+\        z \\<in> Infinitesimal; yb \\<in> Infinitesimal |] \
+\     ==> x + y \\<approx> #0";
 by (forw_inst_tac [("c1","z")] (hypreal_mult_right_cancel RS iffD2) 1 
     THEN assume_tac 1);
 by (thin_tac "(x + y) / z = hypreal_of_real D + yb" 1);
@@ -1128,8 +1127,8 @@
 qed "incrementI2";
 
 (* The Increment theorem -- Keisler p. 65 *)
-Goal "[| NSDERIV f x :> D; h: Infinitesimal; h ~= #0 |] \
-\     ==> EX e: Infinitesimal. increment f x h = hypreal_of_real(D)*h + e*h";
+Goal "[| NSDERIV f x :> D; h \\<in> Infinitesimal; h \\<noteq> #0 |] \
+\     ==> \\<exists>e \\<in> Infinitesimal. increment f x h = hypreal_of_real(D)*h + e*h";
 by (forw_inst_tac [("h","h")] incrementI2 1 THEN rewtac nsderiv_def);
 by (dtac bspec 1 THEN Auto_tac);
 by (dtac (bex_Infinitesimal_iff2 RS iffD2) 1 THEN Step_tac 1);
@@ -1144,15 +1143,15 @@
               simpset() addsimps [hypreal_add_mult_distrib]));
 qed "increment_thm";
 
-Goal "[| NSDERIV f x :> D; h @= #0; h ~= #0 |] \
-\     ==> EX e: Infinitesimal. increment f x h = \
+Goal "[| NSDERIV f x :> D; h \\<approx> #0; h \\<noteq> #0 |] \
+\     ==> \\<exists>e \\<in> Infinitesimal. increment f x h = \
 \             hypreal_of_real(D)*h + e*h";
 by (blast_tac (claset() addSDs [mem_infmal_iff RS iffD2] 
                         addSIs [increment_thm]) 1);
 qed "increment_thm2";
 
-Goal "[| NSDERIV f x :> D; h @= #0; h ~= #0 |] \
-\     ==> increment f x h @= #0";
+Goal "[| NSDERIV f x :> D; h \\<approx> #0; h \\<noteq> #0 |] \
+\     ==> increment f x h \\<approx> #0";
 by (dtac increment_thm2 1 THEN auto_tac (claset() addSIs 
     [Infinitesimal_HFinite_mult2,HFinite_add],simpset() addsimps 
     [hypreal_add_mult_distrib RS sym,mem_infmal_iff RS sym]));
@@ -1172,8 +1171,8 @@
 Goalw [nsderiv_def] 
       "[| NSDERIV g x :> D; \
 \              (*f* g) (hypreal_of_real(x) + xa) = hypreal_of_real(g x);\
-\              xa : Infinitesimal;\
-\              xa ~= #0 \
+\              xa \\<in> Infinitesimal;\
+\              xa \\<noteq> #0 \
 \           |] ==> D = #0";
 by (dtac bspec 1);
 by Auto_tac;
@@ -1181,8 +1180,8 @@
 
 (* can be proved differently using NSLIM_isCont_iff *)
 Goalw [nsderiv_def] 
-     "[| NSDERIV f x :> D;  h: Infinitesimal;  h ~= #0 |]  \
-\     ==> (*f* f) (hypreal_of_real(x) + h) + -hypreal_of_real(f x) @= #0";    
+     "[| NSDERIV f x :> D;  h \\<in> Infinitesimal;  h \\<noteq> #0 |]  \
+\     ==> (*f* f) (hypreal_of_real(x) + h) + -hypreal_of_real(f x) \\<approx> #0";    
 by (asm_full_simp_tac (simpset() addsimps 
     [mem_infmal_iff RS sym]) 1);
 by (rtac Infinitesimal_ratio 1);
@@ -1194,16 +1193,16 @@
    from one version of differentiability 
  
                 f(x) - f(a)
-              --------------- @= Db
+              --------------- \\<approx> Db
                   x - a
  ---------------------------------------------------------------*)
 Goal "[| NSDERIV f (g x) :> Da; \
-\        (*f* g) (hypreal_of_real(x) + xa) ~= hypreal_of_real (g x); \
-\        (*f* g) (hypreal_of_real(x) + xa) @= hypreal_of_real (g x) \
+\        (*f* g) (hypreal_of_real(x) + xa) \\<noteq> hypreal_of_real (g x); \
+\        (*f* g) (hypreal_of_real(x) + xa) \\<approx> hypreal_of_real (g x) \
 \     |] ==> ((*f* f) ((*f* g) (hypreal_of_real(x) + xa)) \
 \                  + - hypreal_of_real (f (g x))) \
 \             / ((*f* g) (hypreal_of_real(x) + xa) + - hypreal_of_real (g x)) \
-\            @= hypreal_of_real(Da)";
+\            \\<approx> hypreal_of_real(Da)";
 by (auto_tac (claset(),
        simpset() addsimps [NSDERIV_NSLIM_iff2, NSLIM_def]));
 qed "NSDERIVD1";
@@ -1212,18 +1211,18 @@
    from other version of differentiability 
 
                 f(x + h) - f(x)
-               ----------------- @= Db
+               ----------------- \\<approx> Db
                        h
  --------------------------------------------------------------*)
-Goal "[| NSDERIV g x :> Db; xa: Infinitesimal; xa ~= #0 |] \
+Goal "[| NSDERIV g x :> Db; xa \\<in> Infinitesimal; xa \\<noteq> #0 |] \
 \     ==> ((*f* g) (hypreal_of_real(x) + xa) + - hypreal_of_real(g x)) / xa \
-\         @= hypreal_of_real(Db)";
+\         \\<approx> hypreal_of_real(Db)";
 by (auto_tac (claset(),
     simpset() addsimps [NSDERIV_NSLIM_iff, NSLIM_def, 
 		hypreal_of_real_zero, mem_infmal_iff, starfun_lambda_cancel]));
 qed "NSDERIVD2";
 
-Goal "(z::hypreal) ~= 0 ==> x*y = (x*inverse(z))*(z*y)";
+Goal "(z::hypreal) \\<noteq> 0 ==> x*y = (x*inverse(z))*(z*y)";
 by Auto_tac;  
 qed "lemma_chain";
 
@@ -1315,9 +1314,9 @@
                     Power of -1 
  ---------------------------------------------------------------*)
 
-(*Can't get rid of x ~= #0 because it isn't continuous at zero*)
+(*Can't get rid of x \\<noteq> #0 because it isn't continuous at zero*)
 Goalw [nsderiv_def]
-     "x ~= #0 ==> NSDERIV (%x. inverse(x)) x :> (- (inverse x ^ 2))";
+     "x \\<noteq> #0 ==> NSDERIV (%x. inverse(x)) x :> (- (inverse x ^ 2))";
 by (rtac ballI 1 THEN Asm_full_simp_tac 1 THEN Step_tac 1);
 by (forward_tac [Infinitesimal_add_not_zero] 1);
 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 2); 
@@ -1346,7 +1345,7 @@
 qed "NSDERIV_inverse";
 
 
-Goal "x ~= #0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ 2))";
+Goal "x \\<noteq> #0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ 2))";
 by (asm_simp_tac (simpset() addsimps [NSDERIV_inverse,
          NSDERIV_DERIV_iff RS sym] delsimps [realpow_Suc]) 1);
 qed "DERIV_inverse";
@@ -1354,7 +1353,7 @@
 (*--------------------------------------------------------------
         Derivative of inverse 
  -------------------------------------------------------------*)
-Goal "[| DERIV f x :> d; f(x) ~= #0 |] \
+Goal "[| DERIV f x :> d; f(x) \\<noteq> #0 |] \
 \     ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))";
 by (rtac (real_mult_commute RS subst) 1);
 by (asm_simp_tac (simpset() addsimps [real_minus_mult_eq1,
@@ -1364,7 +1363,7 @@
 by (blast_tac (claset() addSIs [DERIV_chain,DERIV_inverse]) 1);
 qed "DERIV_inverse_fun";
 
-Goal "[| NSDERIV f x :> d; f(x) ~= #0 |] \
+Goal "[| NSDERIV f x :> d; f(x) \\<noteq> #0 |] \
 \     ==> NSDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))";
 by (asm_full_simp_tac (simpset() addsimps [NSDERIV_DERIV_iff,
             DERIV_inverse_fun] delsimps [realpow_Suc]) 1);
@@ -1373,7 +1372,7 @@
 (*--------------------------------------------------------------
         Derivative of quotient 
  -------------------------------------------------------------*)
-Goal "[| DERIV f x :> d; DERIV g x :> e; g(x) ~= #0 |] \
+Goal "[| DERIV f x :> d; DERIV g x :> e; g(x) \\<noteq> #0 |] \
 \      ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) + -(e*f(x))) / (g(x) ^ 2)";
 by (dres_inst_tac [("f","g")] DERIV_inverse_fun 1);
 by (dtac DERIV_mult 2);
@@ -1385,7 +1384,7 @@
                  real_minus_mult_eq2 RS sym]) 1);
 qed "DERIV_quotient";
 
-Goal "[| NSDERIV f x :> d; DERIV g x :> e; g(x) ~= #0 |] \
+Goal "[| NSDERIV f x :> d; DERIV g x :> e; g(x) \\<noteq> #0 |] \
 \      ==> NSDERIV (%y. f(y) / (g y)) x :> (d*g(x) \
 \                           + -(e*f(x))) / (g(x) ^ 2)";
 by (asm_full_simp_tac (simpset() addsimps [NSDERIV_DERIV_iff,
@@ -1397,25 +1396,25 @@
 (* ------------------------------------------------------------------------ *)
 
 Goal "(DERIV f x :> l) = \
-\     (EX g. (ALL z. f z - f x = g z * (z - x)) & isCont g x & g x = l)";
+\     (\\<exists>g. (\\<forall>z. f z - f x = g z * (z - x)) & isCont g x & g x = l)";
 by Safe_tac;
 by (res_inst_tac 
     [("x","%z. if  z = x then l else (f(z) - f(x)) / (z - x)")] exI 1);
 by (auto_tac (claset(),simpset() addsimps [real_mult_assoc,
-    ARITH_PROVE "z ~= x ==> z - x ~= (#0::real)"]));
+    ARITH_PROVE "z \\<noteq> x ==> z - x \\<noteq> (#0::real)"]));
 by (auto_tac (claset(),simpset() addsimps [isCont_iff,DERIV_iff]));
 by (ALLGOALS(rtac (LIM_equal RS iffD1)));
 by (auto_tac (claset(),simpset() addsimps [real_diff_def,real_mult_assoc]));
 qed "CARAT_DERIV";
 
 Goal "NSDERIV f x :> l ==> \
-\     EX g. (ALL z. f z - f x = g z * (z - x)) & isNSCont g x & g x = l";
+\     \\<exists>g. (\\<forall>z. f z - f x = g z * (z - x)) & isNSCont g x & g x = l";
 by (auto_tac (claset(),simpset() addsimps [NSDERIV_DERIV_iff,
     isNSCont_isCont_iff,CARAT_DERIV]));
 qed "CARAT_NSDERIV";
 
 (* How about a NS proof? *)
-Goal "(ALL z. f z - f x = g z * (z - x)) & isNSCont g x & g x = l \
+Goal "(\\<forall>z. f z - f x = g z * (z - x)) & isNSCont g x & g x = l \
 \     ==> NSDERIV f x :> l";
 by (auto_tac (claset(), 
               simpset() delsimprocs real_cancel_factor
@@ -1434,14 +1433,14 @@
 (* All considerably tidied by lcp                                           *)
 (*--------------------------------------------------------------------------*)
 
-Goal "(ALL n. (f::nat=>real) n <= f (Suc n)) --> f m <= f(m + no)";
+Goal "(\\<forall>n. (f::nat=>real) n \\<le> f (Suc n)) --> f m \\<le> f(m + no)";
 by (induct_tac "no" 1);
 by (auto_tac (claset() addIs [order_trans], simpset()));
 qed_spec_mp "lemma_f_mono_add";
 
-Goal "[| ALL n. f(n) <= f(Suc n); \
-\        ALL n. g(Suc n) <= g(n); \
-\        ALL n. f(n) <= g(n) |] \
+Goal "[| \\<forall>n. f(n) \\<le> f(Suc n); \
+\        \\<forall>n. g(Suc n) \\<le> g(n); \
+\        \\<forall>n. f(n) \\<le> g(n) |] \
 \     ==> Bseq f";
 by (res_inst_tac [("k","f 0"),("K","g 0")] BseqI2 1 THEN rtac allI 1);
 by (induct_tac "n" 1);
@@ -1451,25 +1450,25 @@
 by (auto_tac (claset() addIs [order_trans], simpset()));
 qed "f_inc_g_dec_Beq_f";
 
-Goal "[| ALL n. f(n) <= f(Suc n); \
-\        ALL n. g(Suc n) <= g(n); \
-\        ALL n. f(n) <= g(n) |] \
+Goal "[| \\<forall>n. f(n) \\<le> f(Suc n); \
+\        \\<forall>n. g(Suc n) \\<le> g(n); \
+\        \\<forall>n. f(n) \\<le> g(n) |] \
 \     ==> Bseq g";
 by (stac (Bseq_minus_iff RS sym) 1);
 by (res_inst_tac [("g","%x. -(f x)")] f_inc_g_dec_Beq_f 1); 
 by Auto_tac;  
 qed "f_inc_g_dec_Beq_g";
 
-Goal "[| ALL n. f n <= f (Suc n);  convergent f |] ==> f n <= lim f";
+Goal "[| \\<forall>n. f n \\<le> f (Suc n);  convergent f |] ==> f n \\<le> lim f";
 by (rtac real_leI 1);
 by (auto_tac (claset(), 
       simpset() addsimps [convergent_LIMSEQ_iff, LIMSEQ_iff, monoseq_Suc]));
 by (dtac real_less_sum_gt_zero 1);
 by (dres_inst_tac [("x","f n + - lim f")] spec 1);
 by Safe_tac;
-by (dres_inst_tac [("P","%na. no<=na --> ?Q na"),("x","no + n")] spec 2);
+by (dres_inst_tac [("P","%na. no\\<le>na --> ?Q na"),("x","no + n")] spec 2);
 by Auto_tac;
-by (subgoal_tac "lim f <= f(no + n)" 1);
+by (subgoal_tac "lim f \\<le> f(no + n)" 1);
 by (induct_tac "no" 2);
 by (auto_tac (claset() addIs [order_trans],
               simpset() addsimps [real_diff_def, real_abs_def]));
@@ -1483,18 +1482,18 @@
 by (asm_full_simp_tac (simpset() addsimps [convergent_LIMSEQ_iff]) 1); 
 qed "lim_uminus";
 
-Goal "[| ALL n. g(Suc n) <= g(n);  convergent g |] ==> lim g <= g n";
-by (subgoal_tac "- (g n) <= - (lim g)" 1);
+Goal "[| \\<forall>n. g(Suc n) \\<le> g(n);  convergent g |] ==> lim g \\<le> g n";
+by (subgoal_tac "- (g n) \\<le> - (lim g)" 1);
 by (cut_inst_tac [("f", "%x. - (g x)")] f_inc_imp_le_lim 2);
 by (auto_tac (claset(), 
               simpset() addsimps [lim_uminus, convergent_minus_iff RS sym]));  
 qed "g_dec_imp_lim_le";
 
-Goal "[| ALL n. f(n) <= f(Suc n); \
-\        ALL n. g(Suc n) <= g(n); \
-\        ALL n. f(n) <= g(n) |] \
-\     ==> EX l m. l <= m &  ((ALL n. f(n) <= l) & f ----> l) & \
-\                           ((ALL n. m <= g(n)) & g ----> m)";
+Goal "[| \\<forall>n. f(n) \\<le> f(Suc n); \
+\        \\<forall>n. g(Suc n) \\<le> g(n); \
+\        \\<forall>n. f(n) \\<le> g(n) |] \
+\     ==> \\<exists>l m. l \\<le> m &  ((\\<forall>n. f(n) \\<le> l) & f ----> l) & \
+\                           ((\\<forall>n. m \\<le> g(n)) & g ----> m)";
 by (subgoal_tac "monoseq f & monoseq g" 1);
 by (force_tac (claset(), simpset() addsimps [LIMSEQ_iff,monoseq_Suc]) 2);
 by (subgoal_tac "Bseq f & Bseq g" 1);
@@ -1509,12 +1508,12 @@
                                   convergent_LIMSEQ_iff]));  
 qed "lemma_nest";
 
-Goal "[| ALL n. f(n) <= f(Suc n); \
-\        ALL n. g(Suc n) <= g(n); \
-\        ALL n. f(n) <= g(n); \
+Goal "[| \\<forall>n. f(n) \\<le> f(Suc n); \
+\        \\<forall>n. g(Suc n) \\<le> g(n); \
+\        \\<forall>n. f(n) \\<le> g(n); \
 \        (%n. f(n) - g(n)) ----> #0 |] \
-\     ==> EX l. ((ALL n. f(n) <= l) & f ----> l) & \
-\               ((ALL n. l <= g(n)) & g ----> l)";
+\     ==> \\<exists>l. ((\\<forall>n. f(n) \\<le> l) & f ----> l) & \
+\               ((\\<forall>n. l \\<le> g(n)) & g ----> l)";
 by (dtac lemma_nest 1 THEN Auto_tac);
 by (subgoal_tac "l = m" 1);
 by (dres_inst_tac [("X","f")] LIMSEQ_diff 2);
@@ -1522,23 +1521,23 @@
 qed "lemma_nest_unique";
 
 
-Goal "a <= b ==> \
-\  ALL n. fst (Bolzano_bisect P a b n) <= snd (Bolzano_bisect P a b n)";
+Goal "a \\<le> b ==> \
+\  \\<forall>n. fst (Bolzano_bisect P a b n) \\<le> snd (Bolzano_bisect P a b n)";
 by (rtac allI 1);
 by (induct_tac "n" 1);
 by (auto_tac (claset(), simpset() addsimps [Let_def, split_def]));  
 qed "Bolzano_bisect_le";
 
-Goal "a <= b ==> \
-\  ALL n. fst(Bolzano_bisect P a b n) <= fst (Bolzano_bisect P a b (Suc n))";
+Goal "a \\<le> b ==> \
+\  \\<forall>n. fst(Bolzano_bisect P a b n) \\<le> fst (Bolzano_bisect P a b (Suc n))";
 by (rtac allI 1);
 by (induct_tac "n" 1);
 by (auto_tac (claset(), 
               simpset() addsimps [Bolzano_bisect_le, Let_def, split_def]));  
 qed "Bolzano_bisect_fst_le_Suc";
 
-Goal "a <= b ==> \
-\  ALL n. snd(Bolzano_bisect P a b (Suc n)) <= snd (Bolzano_bisect P a b n)";
+Goal "a \\<le> b ==> \
+\  \\<forall>n. snd(Bolzano_bisect P a b (Suc n)) \\<le> snd (Bolzano_bisect P a b n)";
 by (rtac allI 1);
 by (induct_tac "n" 1);
 by (auto_tac (claset(), 
@@ -1551,7 +1550,7 @@
 by Auto_tac;  
 qed "eq_divide_2_times_iff";
 
-Goal "a <= b ==> \
+Goal "a \\<le> b ==> \
 \     snd(Bolzano_bisect P a b n) - fst(Bolzano_bisect P a b n) = \
 \     (b-a) / (#2 ^ n)";
 by (induct_tac "n" 1);
@@ -1568,8 +1567,8 @@
 
 (*P_prem is a looping simprule, so it works better if it isn't an assumption*)
 val P_prem::notP_prem::rest =
-Goal "[| !!a b c. [| P(a,b); P(b,c); a <= b; b <= c|] ==> P(a,c); \
-\        ~ P(a,b);  a <= b |] ==> \
+Goal "[| !!a b c. [| P(a,b); P(b,c); a \\<le> b; b \\<le> c|] ==> P(a,c); \
+\        ~ P(a,b);  a \\<le> b |] ==> \
 \     ~ P(fst(Bolzano_bisect P a b n), snd(Bolzano_bisect P a b n))";
 by (cut_facts_tac rest 1);
 by (induct_tac "n" 1);
@@ -1582,17 +1581,17 @@
 qed "not_P_Bolzano_bisect";
 
 (*Now we re-package P_prem as a formula*)
-Goal "[| ALL a b c. P(a,b) & P(b,c) & a <= b & b <= c --> P(a,c); \
-\        ~ P(a,b);  a <= b |] ==> \
-\     ALL n. ~ P(fst(Bolzano_bisect P a b n), snd(Bolzano_bisect P a b n))";
+Goal "[| \\<forall>a b c. P(a,b) & P(b,c) & a \\<le> b & b \\<le> c --> P(a,c); \
+\        ~ P(a,b);  a \\<le> b |] ==> \
+\     \\<forall>n. ~ P(fst(Bolzano_bisect P a b n), snd(Bolzano_bisect P a b n))";
 by (blast_tac (claset() addSEs [not_P_Bolzano_bisect RSN (2,rev_notE)]) 1); 
 qed "not_P_Bolzano_bisect'";
 
 
-Goal "[| ALL a b c. P(a,b) & P(b,c) & a <= b & b <= c --> P(a,c); \
-\        ALL x. EX d::real. #0 < d & \
-\               (ALL a b. a <= x & x <= b & (b - a) < d --> P(a,b)); \
-\        a <= b |]  \
+Goal "[| \\<forall>a b c. P(a,b) & P(b,c) & a \\<le> b & b \\<le> c --> P(a,c); \
+\        \\<forall>x. \\<exists>d::real. #0 < d & \
+\               (\\<forall>a b. a \\<le> x & x \\<le> b & (b - a) < d --> P(a,b)); \
+\        a \\<le> b |]  \
 \     ==> P(a,b)";
 by (rtac (inst "P1" "P" Bolzano_nest_unique RS exE) 1);
 by (REPEAT (assume_tac 1));
@@ -1626,10 +1625,10 @@
 qed "lemma_BOLZANO";
 
 
-Goal "((ALL a b c. (a <= b & b <= c & P(a,b) & P(b,c)) --> P(a,c)) & \
-\      (ALL x. EX d::real. #0 < d & \
-\               (ALL a b. a <= x & x <= b & (b - a) < d --> P(a,b)))) \
-\     --> (ALL a b. a <= b --> P(a,b))";
+Goal "((\\<forall>a b c. (a \\<le> b & b \\<le> c & P(a,b) & P(b,c)) --> P(a,c)) & \
+\      (\\<forall>x. \\<exists>d::real. #0 < d & \
+\               (\\<forall>a b. a \\<le> x & x \\<le> b & (b - a) < d --> P(a,b)))) \
+\     --> (\\<forall>a b. a \\<le> b --> P(a,b))";
 by (Clarify_tac 1);
 by (blast_tac (claset() addIs [lemma_BOLZANO]) 1); 
 qed "lemma_BOLZANO2";
@@ -1639,21 +1638,21 @@
 (* Intermediate Value Theorem (prove contrapositive by bisection)             *)
 (*----------------------------------------------------------------------------*)
 
-Goal "[| f(a) <= y & y <= f(b); \
-\        a <= b; \
-\        (ALL x. a <= x & x <= b --> isCont f x) |] \
-\     ==> EX x. a <= x & x <= b & f(x) = y";
+Goal "[| f(a) \\<le> y & y \\<le> f(b); \
+\        a \\<le> b; \
+\        (\\<forall>x. a \\<le> x & x \\<le> b --> isCont f x) |] \
+\     ==> \\<exists>x. a \\<le> x & x \\<le> b & f(x) = y";
 by (rtac contrapos_pp 1);
 by (assume_tac 1);
 by (cut_inst_tac
-    [("P","%(u,v). a <= u & u <= v & v <= b --> ~(f(u) <= y & y <= f(v))")] 
+    [("P","%(u,v). a \\<le> u & u \\<le> v & v \\<le> b --> ~(f(u) \\<le> y & y \\<le> f(v))")] 
     lemma_BOLZANO2 1);
 by Safe_tac;
 by (ALLGOALS(Asm_full_simp_tac));
 by (Blast_tac 2);
 by (asm_full_simp_tac (simpset() addsimps [isCont_iff,LIM_def]) 1);
 by (rtac ccontr 1);
-by (subgoal_tac "a <= x & x <= b" 1);
+by (subgoal_tac "a \\<le> x & x \\<le> b" 1);
 by (Asm_full_simp_tac 2);
 by (dres_inst_tac [("P", "%d. #0<d --> ?P d"),("x","#1")] spec 2);
 by (Step_tac 2);
@@ -1662,7 +1661,7 @@
 by (REPEAT(blast_tac (claset() addIs [order_trans]) 2));
 by (REPEAT(dres_inst_tac [("x","x")] spec 1));
 by (Asm_full_simp_tac 1);
-by (dres_inst_tac [("P", "%r. ?P r --> (EX s. #0<s & ?Q r s)"),
+by (dres_inst_tac [("P", "%r. ?P r --> (\\<exists>s. #0<s & ?Q r s)"),
                    ("x","abs(y - f x)")] spec 1);
 by Safe_tac;
 by (asm_full_simp_tac (simpset() addsimps []) 1);
@@ -1673,34 +1672,34 @@
 by (dres_inst_tac [("x","ba - x")] spec 1);
 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [abs_iff])));
 by (dres_inst_tac [("x","aa - x")] spec 1);
-by (case_tac "x <= aa" 1);
+by (case_tac "x \\<le> aa" 1);
 by (ALLGOALS Asm_full_simp_tac);
 by (dres_inst_tac [("z","x"),("w","aa")] real_le_anti_sym 1);
 by (assume_tac 1 THEN Asm_full_simp_tac 1);
 qed "IVT";
 
 
-Goal "[| f(b) <= y & y <= f(a); \
-\        a <= b; \
-\        (ALL x. a <= x & x <= b --> isCont f x) \
-\     |] ==> EX x. a <= x & x <= b & f(x) = y";
-by (subgoal_tac "- f a <= -y & -y <= - f b" 1);
-by (thin_tac "f b <= y & y <= f a" 1);
+Goal "[| f(b) \\<le> y & y \\<le> f(a); \
+\        a \\<le> b; \
+\        (\\<forall>x. a \\<le> x & x \\<le> b --> isCont f x) \
+\     |] ==> \\<exists>x. a \\<le> x & x \\<le> b & f(x) = y";
+by (subgoal_tac "- f a \\<le> -y & -y \\<le> - f b" 1);
+by (thin_tac "f b \\<le> y & y \\<le> f a" 1);
 by (dres_inst_tac [("f","%x. - f x")] IVT 1);
 by (auto_tac (claset() addIs [isCont_minus],simpset()));
 qed "IVT2";
 
 
 (*HOL style here: object-level formulations*)
-Goal "(f(a) <= y & y <= f(b) & a <= b & \
-\     (ALL x. a <= x & x <= b --> isCont f x)) \
-\     --> (EX x. a <= x & x <= b & f(x) = y)";
+Goal "(f(a) \\<le> y & y \\<le> f(b) & a \\<le> b & \
+\     (\\<forall>x. a \\<le> x & x \\<le> b --> isCont f x)) \
+\     --> (\\<exists>x. a \\<le> x & x \\<le> b & f(x) = y)";
 by (blast_tac (claset() addIs [IVT]) 1);
 qed "IVT_objl";
 
-Goal "(f(b) <= y & y <= f(a) & a <= b & \
-\     (ALL x. a <= x & x <= b --> isCont f x)) \
-\     --> (EX x. a <= x & x <= b & f(x) = y)";
+Goal "(f(b) \\<le> y & y \\<le> f(a) & a \\<le> b & \
+\     (\\<forall>x. a \\<le> x & x \\<le> b --> isCont f x)) \
+\     --> (\\<exists>x. a \\<le> x & x \\<le> b & f(x) = y)";
 by (blast_tac (claset() addIs [IVT2]) 1);
 qed "IVT2_objl";
 
@@ -1720,10 +1719,10 @@
 Addsimps [abs_add_one_not_less_self];
 
 
-Goal "[| a <= b; ALL x. a <= x & x <= b --> isCont f x |]\
-\     ==> EX M. ALL x. a <= x & x <= b --> f(x) <= M";
-by (cut_inst_tac [("P","%(u,v). a <= u & u <= v & v <= b --> \
-\                         (EX M. ALL x. u <= x & x <= v --> f x <= M)")] 
+Goal "[| a \\<le> b; \\<forall>x. a \\<le> x & x \\<le> b --> isCont f x |]\
+\     ==> \\<exists>M. \\<forall>x. a \\<le> x & x \\<le> b --> f(x) \\<le> M";
+by (cut_inst_tac [("P","%(u,v). a \\<le> u & u \\<le> v & v \\<le> b --> \
+\                         (\\<exists>M. \\<forall>x. u \\<le> x & x \\<le> v --> f x \\<le> M)")] 
     lemma_BOLZANO2 1);
 by Safe_tac;
 by (ALLGOALS Asm_full_simp_tac);
@@ -1738,12 +1737,12 @@
 by (Clarify_tac 1); 
 by (cut_inst_tac [("x","xb"),("y","xa")] linorder_linear 1);
 by (Force_tac 1); 
-by (case_tac "a <= x & x <= b" 1);
+by (case_tac "a \\<le> x & x \\<le> b" 1);
 by (res_inst_tac [("x","#1")] exI 2);
 by (Force_tac 2); 
 by (asm_full_simp_tac (simpset() addsimps [LIM_def,isCont_iff]) 1);
 by (dres_inst_tac [("x","x")] spec 1 THEN Auto_tac);
-by (thin_tac "ALL M. EX x. a <= x & x <= b & ~ f x <= M" 1);
+by (thin_tac "\\<forall>M. \\<exists>x. a \\<le> x & x \\<le> b & ~ f x \\<le> M" 1);
 by (dres_inst_tac [("x","#1")] spec 1);
 by Auto_tac;  
 by (res_inst_tac [("x","s")] exI 1 THEN Clarify_tac 1);
@@ -1759,15 +1758,15 @@
 (* Refine the above to existence of least upper bound                         *)
 (*----------------------------------------------------------------------------*)
 
-Goal "((EX x. x : S) & (EX y. isUb UNIV S (y::real))) --> \
-\     (EX t. isLub UNIV S t)";
+Goal "((\\<exists>x. x \\<in> S) & (\\<exists>y. isUb UNIV S (y::real))) --> \
+\     (\\<exists>t. isLub UNIV S t)";
 by (blast_tac (claset() addIs [reals_complete]) 1);
 qed "lemma_reals_complete";
 
-Goal "[| a <= b; ALL x. a <= x & x <= b --> isCont f x |] \
-\        ==> EX M. (ALL x. a <= x & x <= b --> f(x) <= M) & \
-\                  (ALL N. N < M --> (EX x. a <= x & x <= b & N < f(x)))";
-by (cut_inst_tac [("S","Collect (%y. EX x. a <= x & x <= b & y = f x)")]
+Goal "[| a \\<le> b; \\<forall>x. a \\<le> x & x \\<le> b --> isCont f x |] \
+\        ==> \\<exists>M. (\\<forall>x. a \\<le> x & x \\<le> b --> f(x) \\<le> M) & \
+\                  (\\<forall>N. N < M --> (\\<exists>x. a \\<le> x & x \\<le> b & N < f(x)))";
+by (cut_inst_tac [("S","Collect (%y. \\<exists>x. a \\<le> x & x \\<le> b & y = f x)")]
     lemma_reals_complete 1);
 by Auto_tac;
 by (dtac isCont_bounded 1 THEN assume_tac 1);
@@ -1783,38 +1782,38 @@
 (* Now show that it attains its upper bound                                   *)
 (*----------------------------------------------------------------------------*)
 
-Goal "[| a <= b; ALL x. a <= x & x <= b --> isCont f x |] \
-\        ==> EX M. (ALL x. a <= x & x <= b --> f(x) <= M) & \
-\                  (EX x. a <= x & x <= b & f(x) = M)";
+Goal "[| a \\<le> b; \\<forall>x. a \\<le> x & x \\<le> b --> isCont f x |] \
+\        ==> \\<exists>M. (\\<forall>x. a \\<le> x & x \\<le> b --> f(x) \\<le> M) & \
+\                  (\\<exists>x. a \\<le> x & x \\<le> b & f(x) = M)";
 by (ftac isCont_has_Ub 1 THEN assume_tac 1);
 by (Clarify_tac 1);
 by (res_inst_tac [("x","M")] exI 1);
 by (Asm_full_simp_tac 1); 
 by (rtac ccontr 1);
-by (subgoal_tac "ALL x. a <= x & x <= b --> f x < M" 1 THEN Step_tac 1);
+by (subgoal_tac "\\<forall>x. a \\<le> x & x \\<le> b --> f x < M" 1 THEN Step_tac 1);
 by (rtac ccontr 2 THEN dtac real_leI 2);
 by (dres_inst_tac [("z","M")] real_le_anti_sym 2);
 by (REPEAT(Blast_tac 2));
-by (subgoal_tac "ALL x. a <= x & x <= b --> isCont (%x. inverse(M - f x)) x" 1);
+by (subgoal_tac "\\<forall>x. a \\<le> x & x \\<le> b --> isCont (%x. inverse(M - f x)) x" 1);
 by Safe_tac;
 by (EVERY[rtac isCont_inverse 2, rtac isCont_diff 2, rtac notI 4]);
 by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [real_diff_eq_eq])));
 by (Blast_tac 2);
 by (subgoal_tac 
-    "EX k. ALL x. a <= x & x <= b --> (%x. inverse(M - (f x))) x <= k" 1);
+    "\\<exists>k. \\<forall>x. a \\<le> x & x \\<le> b --> (%x. inverse(M - (f x))) x \\<le> k" 1);
 by (rtac isCont_bounded 2);
 by Safe_tac;
-by (subgoal_tac "ALL x. a <= x & x <= b --> #0 < inverse(M - f(x))" 1);
+by (subgoal_tac "\\<forall>x. a \\<le> x & x \\<le> b --> #0 < inverse(M - f(x))" 1);
 by (Asm_full_simp_tac 1); 
 by Safe_tac;
 by (asm_full_simp_tac (simpset() addsimps [real_less_diff_eq]) 2);
 by (subgoal_tac 
-    "ALL x. a <= x & x <= b --> (%x. inverse(M - (f x))) x < (k + #1)" 1);
+    "\\<forall>x. a \\<le> x & x \\<le> b --> (%x. inverse(M - (f x))) x < (k + #1)" 1);
 by Safe_tac;
 by (res_inst_tac [("y","k")] order_le_less_trans 2);
 by (asm_full_simp_tac (simpset() addsimps [real_zero_less_one]) 3);
 by (Asm_full_simp_tac 2); 
-by (subgoal_tac "ALL x. a <= x & x <= b --> \
+by (subgoal_tac "\\<forall>x. a \\<le> x & x \\<le> b --> \
 \                inverse(k + #1) < inverse((%x. inverse(M - (f x))) x)" 1);
 by Safe_tac;
 by (rtac real_inverse_less_swap 2);
@@ -1839,10 +1838,10 @@
 (* Same theorem for lower bound                                               *)
 (*----------------------------------------------------------------------------*)
 
-Goal "[| a <= b; ALL x. a <= x & x <= b --> isCont f x |] \
-\        ==> EX M. (ALL x. a <= x & x <= b --> M <= f(x)) & \
-\                  (EX x. a <= x & x <= b & f(x) = M)";
-by (subgoal_tac "ALL x. a <= x & x <= b --> isCont (%x. -(f x)) x" 1);
+Goal "[| a \\<le> b; \\<forall>x. a \\<le> x & x \\<le> b --> isCont f x |] \
+\        ==> \\<exists>M. (\\<forall>x. a \\<le> x & x \\<le> b --> M \\<le> f(x)) & \
+\                  (\\<exists>x. a \\<le> x & x \\<le> b & f(x) = M)";
+by (subgoal_tac "\\<forall>x. a \\<le> x & x \\<le> b --> isCont (%x. -(f x)) x" 1);
 by (blast_tac (claset() addIs [isCont_minus]) 2);
 by (dres_inst_tac [("f","(%x. -(f x))")] isCont_eq_Ub 1);
 by Safe_tac;
@@ -1854,9 +1853,9 @@
 (* Another version.                                                          *)
 (* ------------------------------------------------------------------------- *)
 
-Goal "[|a <= b; ALL x. a <= x & x <= b --> isCont f x |] \
-\     ==> EX L M. (ALL x. a <= x & x <= b --> L <= f(x) & f(x) <= M) & \
-\         (ALL y. L <= y & y <= M --> (EX x. a <= x & x <= b & (f(x) = y)))";
+Goal "[|a \\<le> b; \\<forall>x. a \\<le> x & x \\<le> b --> isCont f x |] \
+\     ==> \\<exists>L M. (\\<forall>x. a \\<le> x & x \\<le> b --> L \\<le> f(x) & f(x) \\<le> M) & \
+\         (\\<forall>y. L \\<le> y & y \\<le> M --> (\\<exists>x. a \\<le> x & x \\<le> b & (f(x) = y)))";
 by (ftac isCont_eq_Lb 1);
 by (ftac isCont_eq_Ub 2);
 by (REPEAT(assume_tac 1));
@@ -1881,7 +1880,7 @@
 
 Goalw [deriv_def,LIM_def] 
     "[| DERIV f x :> l;  #0 < l |] ==> \
-\      EX d. #0 < d & (ALL h. #0 < h & h < d --> f(x) < f(x + h))";
+\      \\<exists>d. #0 < d & (\\<forall>h. #0 < h & h < d --> f(x) < f(x + h))";
 by (dtac spec 1 THEN Auto_tac);
 by (res_inst_tac [("x","s")] exI 1 THEN Auto_tac);
 by (subgoal_tac "#0 < l*h" 1);
@@ -1895,7 +1894,7 @@
 
 Goalw [deriv_def,LIM_def] 
     "[| DERIV f x :> l;  l < #0 |] ==> \
-\      EX d. #0 < d & (ALL h. #0 < h & h < d --> f(x) < f(x - h))";
+\      \\<exists>d. #0 < d & (\\<forall>h. #0 < h & h < d --> f(x) < f(x - h))";
 by (dres_inst_tac [("x","-l")] spec 1 THEN Auto_tac);
 by (res_inst_tac [("x","s")] exI 1 THEN Auto_tac);
 by (subgoal_tac "l*h < #0" 1);
@@ -1914,7 +1913,7 @@
 
 
 Goal "[| DERIV f x :> l; \
-\        EX d. #0 < d & (ALL y. abs(x - y) < d --> f(y) <= f(x)) |] \
+\        \\<exists>d. #0 < d & (\\<forall>y. abs(x - y) < d --> f(y) \\<le> f(x)) |] \
 \     ==> l = #0";
 by (res_inst_tac [("R1.0","l"),("R2.0","#0")] real_linear_less2 1);
 by Safe_tac;
@@ -1934,7 +1933,7 @@
 (*----------------------------------------------------------------------------*)
 
 Goal "[| DERIV f x :> l; \
-\        EX d::real. #0 < d & (ALL y. abs(x - y) < d --> f(x) <= f(y)) |] \
+\        \\<exists>d::real. #0 < d & (\\<forall>y. abs(x - y) < d --> f(x) \\<le> f(y)) |] \
 \     ==> l = #0";
 by (dtac (DERIV_minus RS DERIV_local_max) 1); 
 by Auto_tac;  
@@ -1945,7 +1944,7 @@
 (*----------------------------------------------------------------------------*)
 
 Goal "[| DERIV f x :> l; \
-\        EX d. #0 < d & (ALL y. abs(x - y) < d --> f(x) = f(y)) |] \
+\        \\<exists>d. #0 < d & (\\<forall>y. abs(x - y) < d --> f(x) = f(y)) |] \
 \     ==> l = #0";
 by (auto_tac (claset() addSDs [DERIV_local_max],simpset()));
 qed "DERIV_local_const";
@@ -1955,7 +1954,7 @@
 (*----------------------------------------------------------------------------*)
 
 Goal "[| a < x;  x < b |] ==> \
-\       EX d::real. #0 < d &  (ALL y. abs(x - y) < d --> a < y & y < b)";
+\       \\<exists>d::real. #0 < d &  (\\<forall>y. abs(x - y) < d --> a < y & y < b)";
 by (simp_tac (simpset() addsimps [abs_interval_iff]) 1);
 by (cut_inst_tac [("x","x - a"),("y","b - x")] linorder_linear 1);
 by Safe_tac;
@@ -1966,7 +1965,7 @@
 qed "lemma_interval_lt";
 
 Goal "[| a < x;  x < b |] ==> \
-\       EX d::real. #0 < d &  (ALL y. abs(x - y) < d --> a <= y & y <= b)";
+\       \\<exists>d::real. #0 < d &  (\\<forall>y. abs(x - y) < d --> a \\<le> y & y \\<le> b)";
 by (dtac lemma_interval_lt 1);
 by Auto_tac;
 by (auto_tac (claset() addSIs [exI] ,simpset()));
@@ -1976,13 +1975,13 @@
             Rolle's Theorem
    If f is defined and continuous on the finite closed interval [a,b]
    and differentiable a least on the open interval (a,b), and f(a) = f(b),
-   then x0 : (a,b) such that f'(x0) = #0
+   then x0 \\<in> (a,b) such that f'(x0) = #0
  ----------------------------------------------------------------------*)
 
 Goal "[| a < b; f(a) = f(b); \
-\        ALL x. a <= x & x <= b --> isCont f x; \
-\        ALL x. a < x & x < b --> f differentiable x \
-\     |] ==> EX z. a < z & z < b & DERIV f z :> #0";
+\        \\<forall>x. a \\<le> x & x \\<le> b --> isCont f x; \
+\        \\<forall>x. a < x & x < b --> f differentiable x \
+\     |] ==> \\<exists>z. a < z & z < b & DERIV f z :> #0";
 by (ftac (order_less_imp_le RS isCont_eq_Ub) 1);
 by (EVERY1[assume_tac,Step_tac]);
 by (ftac (order_less_imp_le RS isCont_eq_Lb) 1);
@@ -1992,8 +1991,8 @@
 by (forw_inst_tac [("a","a"),("x","x")] lemma_interval 1);
 by (EVERY1[assume_tac,etac exE]);
 by (res_inst_tac [("x","x")] exI 1 THEN Asm_full_simp_tac 1);
-by (subgoal_tac "(EX l. DERIV f x :> l) & \
-\        (EX d. #0 < d & (ALL y. abs(x - y) < d --> f(y) <= f(x)))" 1);
+by (subgoal_tac "(\\<exists>l. DERIV f x :> l) & \
+\        (\\<exists>d. #0 < d & (\\<forall>y. abs(x - y) < d --> f(y) \\<le> f(x)))" 1);
 by (Clarify_tac 1 THEN rtac conjI 2);
 by (blast_tac (claset() addIs [differentiableD]) 2);
 by (Blast_tac 2);
@@ -2004,14 +2003,14 @@
 by (forw_inst_tac [("a","a"),("x","xa")] lemma_interval 1);
 by (EVERY1[assume_tac,etac exE]);
 by (res_inst_tac [("x","xa")] exI 1 THEN Asm_full_simp_tac 1);
-by (subgoal_tac "(EX l. DERIV f xa :> l) & \
-\        (EX d. #0 < d & (ALL y. abs(xa - y) < d --> f(xa) <= f(y)))" 1);
+by (subgoal_tac "(\\<exists>l. DERIV f xa :> l) & \
+\        (\\<exists>d. #0 < d & (\\<forall>y. abs(xa - y) < d --> f(xa) \\<le> f(y)))" 1);
 by (Clarify_tac 1 THEN rtac conjI 2);
 by (blast_tac (claset() addIs [differentiableD]) 2);
 by (Blast_tac 2);
 by (ftac DERIV_local_min 1);
 by (EVERY1[Blast_tac,Blast_tac]);
-by (subgoal_tac "ALL x. a <= x & x <= b --> f(x) = f(b)" 1);
+by (subgoal_tac "\\<forall>x. a \\<le> x & x \\<le> b --> f(x) = f(b)" 1);
 by (Clarify_tac 2);
 by (rtac real_le_anti_sym 2);
 by (subgoal_tac "f b = f x" 2);
@@ -2030,8 +2029,8 @@
 by (etac conjE 1);
 by (forw_inst_tac [("a","a"),("x","r")] lemma_interval 1);
 by (EVERY1[assume_tac, etac exE]);
-by (subgoal_tac "(EX l. DERIV f r :> l) & \
-\        (EX d. #0 < d & (ALL y. abs(r - y) < d --> f(r) = f(y)))" 1);
+by (subgoal_tac "(\\<exists>l. DERIV f r :> l) & \
+\        (\\<exists>d. #0 < d & (\\<forall>y. abs(r - y) < d --> f(r) = f(y)))" 1);
 by (Clarify_tac 1 THEN rtac conjI 2);
 by (blast_tac (claset() addIs [differentiableD]) 2);
 by (EVERY1[ftac DERIV_local_const, Blast_tac, Blast_tac]);
@@ -2059,9 +2058,9 @@
 qed "lemma_MVT";
 
 Goal "[| a < b; \
-\        ALL x. a <= x & x <= b --> isCont f x; \
-\        ALL x. a < x & x < b --> f differentiable x |] \
-\     ==>  EX l z. a < z & z < b & DERIV f z :> l & \
+\        \\<forall>x. a \\<le> x & x \\<le> b --> isCont f x; \
+\        \\<forall>x. a < x & x < b --> f differentiable x |] \
+\     ==>  \\<exists>l z. a < z & z < b & DERIV f z :> l & \
 \                  (f(b) - f(a) = (b - a) * l)";
 by (dres_inst_tac [("f","%x. f(x) - (((f(b) - f(a)) / (b - a)) * x)")]
     Rolle 1);
@@ -2098,8 +2097,8 @@
 (*----------------------------------------------------------------------------*)
 
 Goal "[| a < b; \
-\        ALL x. a <= x & x <= b --> isCont f x; \
-\        ALL x. a < x & x < b --> DERIV f x :> #0 |] \
+\        \\<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)";
 by (dtac MVT 1 THEN assume_tac 1);
 by (blast_tac (claset() addIs [differentiableI]) 1);
@@ -2108,9 +2107,9 @@
 qed "DERIV_isconst_end";
 
 Goal "[| a < b; \
-\        ALL x. a <= x & x <= b --> isCont f x; \
-\        ALL x. a < x & x < b --> DERIV f x :> #0 |] \
-\       ==> ALL x. a <= x & x <= b --> f x = f a";
+\        \\<forall>x. a \\<le> x & x \\<le> b --> isCont f x; \
+\        \\<forall>x. a < x & x < b --> DERIV f x :> #0 |] \
+\       ==> \\<forall>x. a \\<le> x & x \\<le> b --> f x = f a";
 by Safe_tac;
 by (dres_inst_tac [("x","a")] order_le_imp_less_or_eq 1);
 by Safe_tac;
@@ -2119,20 +2118,20 @@
 qed "DERIV_isconst1";
 
 Goal "[| a < b; \
-\        ALL x. a <= x & x <= b --> isCont f x; \
-\        ALL x. a < x & x < b --> DERIV f x :> #0; \
-\        a <= x; x <= b |] \
+\        \\<forall>x. a \\<le> x & x \\<le> b --> isCont f x; \
+\        \\<forall>x. a < x & x < b --> DERIV f x :> #0; \
+\        a \\<le> x; x \\<le> b |] \
 \       ==> f x = f a";
 by (blast_tac (claset() addDs [DERIV_isconst1]) 1);
 qed "DERIV_isconst2";
 
-Goal "ALL x. DERIV f x :> #0 ==> f(x) = f(y)";
+Goal "\\<forall>x. DERIV f x :> #0 ==> f(x) = f(y)";
 by (res_inst_tac [("R1.0","x"),("R2.0","y")] real_linear_less2 1);
 by (rtac sym 1);
 by (auto_tac (claset() addIs [DERIV_isCont,DERIV_isconst_end],simpset()));
 qed "DERIV_isconst_all";
 
-Goal "[|a ~= b; ALL x. DERIV f x :> k |] ==> (f(b) - f(a)) = (b - a) * k";
+Goal "[|a \\<noteq> b; \\<forall>x. DERIV f x :> k |] ==> (f(b) - f(a)) = (b - a) * k";
 by (res_inst_tac [("R1.0","a"),("R2.0","b")] real_linear_less2 1);
 by Auto_tac;
 by (ALLGOALS(dres_inst_tac [("f","f")] MVT));
@@ -2143,7 +2142,7 @@
                            real_minus_mult_eq1 RS sym]));
 qed "DERIV_const_ratio_const";
 
-Goal "[|a ~= b; ALL x. DERIV f x :> k |] ==> (f(b) - f(a))/(b - a) = k";
+Goal "[|a \\<noteq> b; \\<forall>x. DERIV f x :> k |] ==> (f(b) - f(a))/(b - a) = k";
 by (res_inst_tac [("c1","b - a")] (real_mult_right_cancel RS iffD1) 1);
 by (auto_tac (claset() addSDs [DERIV_const_ratio_const], 
               simpset() addsimps [real_mult_assoc]));
@@ -2161,7 +2160,7 @@
 
 
 (* Gallileo's "trick": average velocity = av. of end velocities *)
-Goal "[|a ~= (b::real); ALL x. DERIV v x :> k|] \
+Goal "[|a \\<noteq> (b::real); \\<forall>x. DERIV v x :> k|] \
 \     ==> v((a + b)/#2) = (v a + v b)/#2";
 by (res_inst_tac [("R1.0","a"),("R2.0","b")] real_linear_less2 1);
 by Auto_tac;
@@ -2183,16 +2182,16 @@
 (* maximum at an end point, not in the middle.                              *)
 (* ------------------------------------------------------------------------ *)
 
-Goal "[|#0 < d; ALL z. abs(z - x) <= d --> g(f z) = z; \
-\       ALL z. abs(z - x) <= d --> isCont f z |]  \
-\     ==> ~(ALL z. abs(z - x) <= d --> f(z) <= f(x))";
+Goal "[|#0 < d; \\<forall>z. abs(z - x) \\<le> d --> g(f z) = z; \
+\       \\<forall>z. abs(z - x) \\<le> d --> isCont f z |]  \
+\     ==> ~(\\<forall>z. abs(z - x) \\<le> d --> f(z) \\<le> f(x))";
 by (rtac notI 1);
 by (rotate_tac 3 1);
 by (forw_inst_tac [("x","x - d")] spec 1);
 by (forw_inst_tac [("x","x + d")] spec 1);
 by Safe_tac;
 by (cut_inst_tac [("x","f(x - d)"),("y","f(x + d)")] 
-    (ARITH_PROVE "x <= y | y <= (x::real)") 4);
+    (ARITH_PROVE "x \\<le> y | y \\<le> (x::real)") 4);
 by (etac disjE 4);
 by (REPEAT(arith_tac 1));
 by (cut_inst_tac [("f","f"),("a","x - d"),("b","x"),("y","f(x + d)")]
@@ -2222,9 +2221,9 @@
 (* Similar version for lower bound                                          *)
 (* ------------------------------------------------------------------------ *)
 
-Goal "[|#0 < d; ALL z. abs(z - x) <= d --> g(f z) = z; \
-\       ALL z. abs(z - x) <= d --> isCont f z |]  \
-\     ==> ~(ALL z. abs(z - x) <= d --> f(x) <= f(z))";
+Goal "[|#0 < d; \\<forall>z. abs(z - x) \\<le> d --> g(f z) = z; \
+\       \\<forall>z. abs(z - x) \\<le> d --> isCont f z |]  \
+\     ==> ~(\\<forall>z. abs(z - x) \\<le> d --> f(x) \\<le> f(z))";
 by (auto_tac (claset() addSDs [(asm_full_simplify (simpset()) 
     (read_instantiate [("f","%x. - f x"),("g","%y. g(-y)"),("x","x"),("d","d")]
      lemma_isCont_inj))],simpset() addsimps [isCont_minus]));
@@ -2237,21 +2236,21 @@
 
 Addsimps [zero_eq_numeral_0,one_eq_numeral_1];
 
-val lemma_le = ARITH_PROVE "#0 <= (d::real) ==> -d <= d";
+val lemma_le = ARITH_PROVE "#0 \\<le> (d::real) ==> -d \\<le> d";
 
 (* FIXME: awful proof - needs improvement *)
-Goal "[| #0 < d; ALL z. abs(z - x) <= d --> g(f z) = z; \
-\        ALL z. abs(z - x) <= d --> isCont f z |] \
-\      ==> EX e. #0 < e & \
-\                 (ALL y. \
-\                     abs(y - f(x)) <= e --> \
-\                     (EX z. abs(z - x) <= d & (f z = y)))";
+Goal "[| #0 < d; \\<forall>z. abs(z - x) \\<le> d --> g(f z) = z; \
+\        \\<forall>z. abs(z - x) \\<le> d --> isCont f z |] \
+\      ==> \\<exists>e. #0 < e & \
+\                 (\\<forall>y. \
+\                     abs(y - f(x)) \\<le> e --> \
+\                     (\\<exists>z. abs(z - x) \\<le> d & (f z = y)))";
 by (ftac order_less_imp_le 1);
 by (dtac (lemma_le RS (asm_full_simplify (simpset()) (read_instantiate 
     [("f","f"),("a","x - d"),("b","x + d")] isCont_Lb_Ub))) 1);
 by Safe_tac;
 by (asm_full_simp_tac (simpset() addsimps [abs_le_interval_iff]) 1);
-by (subgoal_tac "L <= f x & f x <= M" 1);
+by (subgoal_tac "L \\<le> f x & f x \\<le> M" 1);
 by (dres_inst_tac [("P", "%v. ?P v --> ?Q v & ?R v"), ("x","x")] spec 2);
 by (Asm_full_simp_tac 2);
 by (subgoal_tac "L < f x & f x < M" 1);
@@ -2264,11 +2263,11 @@
 by (res_inst_tac [("x","e")] exI 1);
 by Safe_tac;
 by (asm_full_simp_tac (simpset() addsimps [abs_le_interval_iff]) 1);
-by (dres_inst_tac [("P","%v. ?PP v --> (EX xa. ?Q v xa)"),("x","y")] spec 1);
+by (dres_inst_tac [("P","%v. ?PP v --> (\\<exists>xa. ?Q v xa)"),("x","y")] spec 1);
 by (Step_tac 1 THEN REPEAT(arith_tac 1));
 by (res_inst_tac [("x","xa")] exI 1);
 by (arith_tac 1);
-by (ALLGOALS(etac (ARITH_PROVE "[|x <= y; x ~= y |] ==> x < (y::real)")));
+by (ALLGOALS(etac (ARITH_PROVE "[|x \\<le> y; x \\<noteq> y |] ==> x < (y::real)")));
 by (ALLGOALS(rotate_tac 3));
 by (dtac lemma_isCont_inj2 1);
 by (assume_tac 2);
@@ -2285,16 +2284,16 @@
 (* Continuity of inverse function                                           *)
 (* ------------------------------------------------------------------------ *)
 
-Goal "[| #0 < d; ALL z. abs(z - x) <= d --> g(f(z)) = z; \
-\        ALL z. abs(z - x) <= d --> isCont f z |] \
+Goal "[| #0 < d; \\<forall>z. abs(z - x) \\<le> d --> g(f(z)) = z; \
+\        \\<forall>z. abs(z - x) \\<le> d --> isCont f z |] \
 \     ==> isCont g (f x)";
 by (simp_tac (simpset() addsimps [isCont_iff,LIM_def]) 1);
 by Safe_tac;
 by (dres_inst_tac [("d1.0","r")] (rename_numerals real_lbound_gt_zero) 1);
 by (assume_tac 1 THEN Step_tac 1);
-by (subgoal_tac "ALL z. abs(z - x) <= e --> (g(f z) = z)" 1);
+by (subgoal_tac "\\<forall>z. abs(z - x) \\<le> e --> (g(f z) = z)" 1);
 by (Force_tac 2);
-by (subgoal_tac "ALL z. abs(z - x) <= e --> isCont f z" 1);
+by (subgoal_tac "\\<forall>z. abs(z - x) \\<le> e --> isCont f z" 1);
 by (Force_tac 2);
 by (dres_inst_tac [("d","e")] isCont_inj_range 1);
 by (assume_tac 2 THEN assume_tac 1);
@@ -2306,5 +2305,5 @@
 by Auto_tac;
 by (dtac sym 1 THEN Auto_tac);
 by (arith_tac 1);
-qed "isCont_inverse";
+qed "isCont_inverse_function";
 
diff -r a816fead971a -r 297625089e80 src/HOL/Hyperreal/NSA.ML
--- a/src/HOL/Hyperreal/NSA.ML	Tue Jun 26 17:04:54 2001 +0200
+++ b/src/HOL/Hyperreal/NSA.ML	Tue Jun 26 17:05:10 2001 +0200
@@ -2049,12 +2049,6 @@
               simpset() addsimps [not_real_leE]));
 val lemma = result();
 
-Goal "{n. u < abs (real n)} : FreeUltrafilterNat";
-by (cut_inst_tac [("u","u")] rabs_real_of_nat_le_real_FreeUltrafilterNat 1);
-by (auto_tac (claset() addDs [FreeUltrafilterNat_Compl_mem],
-              simpset() addsimps [lemma]));
-qed "FreeUltrafilterNat_omega";
-
 (*-----------------------------------------------
        Omega is a member of HInfinite
  -----------------------------------------------*)
@@ -2063,7 +2057,6 @@
 by Auto_tac;
 qed "hypreal_omega";
 
-
 Goal "{n. u < real n} : FreeUltrafilterNat";
 by (cut_inst_tac [("u","u")] rabs_real_of_nat_le_real_FreeUltrafilterNat 1);
 by (auto_tac (claset() addDs [FreeUltrafilterNat_Compl_mem],
diff -r a816fead971a -r 297625089e80 src/HOL/UNITY/Guar.ML
--- a/src/HOL/UNITY/Guar.ML	Tue Jun 26 17:04:54 2001 +0200
+++ b/src/HOL/UNITY/Guar.ML	Tue Jun 26 17:05:10 2001 +0200
@@ -253,18 +253,6 @@
 
 Goalw [guar_def]
     "[| ALL i:I. F i : X i guarantees Y i;  OK I F |] \
-\    ==> (JOIN I F) : (INTER I X) guarantees (INTER I Y)";
-by Auto_tac;
-by (ball_tac 1);
-by (rename_tac "i" 1);
-by (dres_inst_tac [("x", "JOIN (I-{i}) F Join G")] spec 1);
-by (auto_tac
-    (claset() addIs [OK_imp_ok],
-     simpset() addsimps [Join_assoc RS sym, JN_Join_diff, JN_absorb]));
-qed "guarantees_JN_INT";
-
-Goalw [guar_def]
-    "[| ALL i:I. F i : X i guarantees Y i;  OK I F |] \
 \    ==> (JOIN I F) : (UNION I X) guarantees (UNION I Y)";
 by Auto_tac;
 by (ball_tac 1);