src/HOL/Hyperreal/Lim.ML

     LIM_add    
  ---------------*)
 Goalw [LIM_def] 
      "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + g(x)) -- x --> (l + m)";
 by (Clarify_tac 1);
-by (REPEAT(dres_inst_tac [("x","r/#2")] spec 1));
+by (REPEAT(dres_inst_tac [("x","r/# 2")] spec 1));
 by (Asm_full_simp_tac 1);
 by (Clarify_tac 1);
 by (res_inst_tac [("R1.0","s"),("R2.0","sa")] 
     real_linear_less2 1);
 by (res_inst_tac [("x","s")] exI 1);

 qed "LIM_add_minus";
 
 (*----------------------------------------------
      LIM_zero
  ----------------------------------------------*)
-Goal "f -- a --> l ==> (%x. f(x) + -l) -- a --> #0";
+Goal "f -- a --> l ==> (%x. f(x) + -l) -- a --> Numeral0";
 by (res_inst_tac [("z1","l")] (rename_numerals (real_add_minus RS subst)) 1);
 by (rtac LIM_add_minus 1 THEN Auto_tac);
 qed "LIM_zero";
 
 (*--------------------------
    Limit not zero
  --------------------------*)
-Goalw [LIM_def] "k \\<noteq> #0 ==> ~ ((%x. k) -- x --> #0)";
-by (res_inst_tac [("R1.0","k"),("R2.0","#0")] real_linear_less2 1);
+Goalw [LIM_def] "k \\<noteq> Numeral0 ==> ~ ((%x. k) -- x --> Numeral0)";
+by (res_inst_tac [("R1.0","k"),("R2.0","Numeral0")] real_linear_less2 1);
 by (auto_tac (claset(), simpset() addsimps [real_abs_def]));
 by (res_inst_tac [("x","-k")] exI 1);
 by (res_inst_tac [("x","k")] exI 2);
 by Auto_tac;
 by (ALLGOALS(dres_inst_tac [("y","s")] real_dense));
 by Safe_tac;
 by (ALLGOALS(res_inst_tac [("x","r + x")] exI));
 by Auto_tac;  
 qed "LIM_not_zero";
 
-(* [| k \\<noteq> #0; (%x. k) -- x --> #0 |] ==> R *)
+(* [| k \\<noteq> Numeral0; (%x. k) -- x --> Numeral0 |] ==> R *)
 bind_thm("LIM_not_zeroE", LIM_not_zero RS notE);
 
 Goal "(%x. k) -- x --> L ==> k = L";
 by (rtac ccontr 1);
 by (dtac LIM_zero 1);

 
 (*-------------
     LIM_mult_zero
  -------------*)
 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);
+     "[| f -- x --> Numeral0; g -- x --> Numeral0 |] ==> (%x. f(x)*g(x)) -- x --> Numeral0";
+by Safe_tac;
+by (dres_inst_tac [("x","Numeral1")] spec 1);
 by (dres_inst_tac [("x","r")] spec 1);
 by (cut_facts_tac [real_zero_less_one] 1);
 by (asm_full_simp_tac (simpset() addsimps 
     [abs_mult]) 1);
 by (Clarify_tac 1);

      "[| \\<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 |] \
+Goal "[| (%x. f(x) + -g(x)) -- a --> Numeral0;  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";
 

  
 (*---------------------------------------------------------------------
     Limit: NS definition ==> standard definition
  ---------------------------------------------------------------------*)
 
-Goal "\\<forall>s. #0 < s --> (\\<exists>xa.  xa \\<noteq> x & \
+Goal "\\<forall>s. Numeral0 < 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 "\\<forall>s. #0 < s --> (\\<exists>xa.  xa \\<noteq> x & \
+Goal "\\<forall>s. Numeral0 < 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);

 
 (*-----------------------------
     NSLIM_inverse
  -----------------------------*)
 Goalw [NSLIM_def] 
-     "[| f -- a --NS> L;  L \\<noteq> #0 |] \
+     "[| f -- a --NS> L;  L \\<noteq> Numeral0 |] \
 \     ==> (%x. inverse(f(x))) -- a --NS> (inverse L)";
 by (Clarify_tac 1);
 by (dtac spec 1);
 by (auto_tac (claset(), 
               simpset() addsimps [hypreal_of_real_approx_inverse]));  
 qed "NSLIM_inverse";
 
 Goal "[| f -- a --> L; \
-\        L \\<noteq> #0 |] ==> (%x. inverse(f(x))) -- a --> (inverse L)";
+\        L \\<noteq> Numeral0 |] ==> (%x. inverse(f(x))) -- a --> (inverse L)";
 by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, NSLIM_inverse]) 1);
 qed "LIM_inverse";
 
 (*------------------------------
     NSLIM_zero
  ------------------------------*)
-Goal "f -- a --NS> l ==> (%x. f(x) + -l) -- a --NS> #0";
+Goal "f -- a --NS> l ==> (%x. f(x) + -l) -- a --NS> Numeral0";
 by (res_inst_tac [("z1","l")] (rename_numerals (real_add_minus RS subst)) 1);
 by (rtac NSLIM_add_minus 1 THEN Auto_tac);
 qed "NSLIM_zero";
 
-Goal "f -- a --> l ==> (%x. f(x) + -l) -- a --> #0";
+Goal "f -- a --> l ==> (%x. f(x) + -l) -- a --> Numeral0";
 by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, NSLIM_zero]) 1);
 qed "LIM_zero2";
 
-Goal "(%x. f(x) - l) -- x --NS> #0 ==> f -- x --NS> l";
+Goal "(%x. f(x) - l) -- x --NS> Numeral0 ==> f -- x --NS> l";
 by (dres_inst_tac [("g","%x. l"),("m","l")] NSLIM_add 1);
 by (auto_tac (claset(),simpset() addsimps [real_diff_def, real_add_assoc]));
 qed "NSLIM_zero_cancel";
 
-Goal "(%x. f(x) - l) -- x --> #0 ==> f -- x --> l";
+Goal "(%x. f(x) - l) -- x --> Numeral0 ==> f -- x --> l";
 by (dres_inst_tac [("g","%x. l"),("m","l")] LIM_add 1);
 by (auto_tac (claset(),simpset() addsimps [real_diff_def, real_add_assoc]));
 qed "LIM_zero_cancel";
 
 
 (*--------------------------
    NSLIM_not_zero
  --------------------------*)
-Goalw [NSLIM_def] "k \\<noteq> #0 ==> ~ ((%x. k) -- x --NS> #0)";
+Goalw [NSLIM_def] "k \\<noteq> Numeral0 ==> ~ ((%x. k) -- x --NS> Numeral0)";
 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 \\<noteq> #0; (%x. k) -- x --NS> #0 |] ==> R *)
+(* [| k \\<noteq> Numeral0; (%x. k) -- x --NS> Numeral0 |] ==> R *)
 bind_thm("NSLIM_not_zeroE", NSLIM_not_zero RS notE);
 
-Goal "k \\<noteq> #0 ==> ~ ((%x. k) -- x --> #0)";
+Goal "k \\<noteq> Numeral0 ==> ~ ((%x. k) -- x --> Numeral0)";
 by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, NSLIM_not_zero]) 1);
 qed "LIM_not_zero2";
 
 (*-------------------------------------
    NSLIM of constant function

 qed "LIM_unique2";
 
 (*--------------------
     NSLIM_mult_zero
  --------------------*)
-Goal "[| f -- x --NS> #0; g -- x --NS> #0 |] \
-\         ==> (%x. f(x)*g(x)) -- x --NS> #0";
+Goal "[| f -- x --NS> Numeral0; g -- x --NS> Numeral0 |] \
+\         ==> (%x. f(x)*g(x)) -- x --NS> Numeral0";
 by (dtac NSLIM_mult 1 THEN Auto_tac);
 qed "NSLIM_mult_zero";
 
 (* we can use the corresponding thm LIM_mult2 *)
 (* for standard definition of limit           *)
 
-Goal "[| f -- x --> #0; g -- x --> #0 |] \
-\     ==> (%x. f(x)*g(x)) -- x --> #0";
+Goal "[| f -- x --> Numeral0; g -- x --> Numeral0 |] \
+\     ==> (%x. f(x)*g(x)) -- x --> Numeral0";
 by (dtac LIM_mult2 1 THEN Auto_tac);
 qed "LIM_mult_zero2";
 
 (*----------------------------
     NSLIM_self

 (*--------------------------------------------------------------------------
                  Alternative definition of continuity
  --------------------------------------------------------------------------*)
 (* Prove equivalence between NS limits - *)
 (* seems easier than using standard def  *)
-Goalw [NSLIM_def] "(f -- a --NS> L) = ((%h. f(a + h)) -- #0 --NS> L)";
+Goalw [NSLIM_def] "(f -- a --NS> L) = ((%h. f(a + h)) -- Numeral0 --NS> L)";
 by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_zero]));
 by (dres_inst_tac [("x","hypreal_of_real a + x")] spec 1);
 by (dres_inst_tac [("x","-hypreal_of_real a + x")] spec 2);
 by Safe_tac;
 by (Asm_full_simp_tac 1);

 by (auto_tac (claset(),
        simpset() addsimps [starfun, hypreal_of_real_def, hypreal_minus,
               hypreal_add, real_add_assoc, approx_refl, hypreal_zero_def]));
 qed "NSLIM_h_iff";
 
-Goal "(f -- a --NS> f a) = ((%h. f(a + h)) -- #0 --NS> f a)";
+Goal "(f -- a --NS> f a) = ((%h. f(a + h)) -- Numeral0 --NS> f a)";
 by (rtac NSLIM_h_iff 1);
 qed "NSLIM_isCont_iff";
 
-Goal "(f -- a --> f a) = ((%h. f(a + h)) -- #0 --> f(a))";
+Goal "(f -- a --> f a) = ((%h. f(a + h)) -- Numeral0 --> f(a))";
 by (simp_tac (simpset() addsimps [LIM_NSLIM_iff, NSLIM_isCont_iff]) 1);
 qed "LIM_isCont_iff";
 
-Goalw [isCont_def] "(isCont f x) = ((%h. f(x + h)) -- #0 --> f(x))";
+Goalw [isCont_def] "(isCont f x) = ((%h. f(x + h)) -- Numeral0 --> f(x))";
 by (simp_tac (simpset() addsimps [LIM_isCont_iff]) 1);
 qed "isCont_iff";
 
 (*--------------------------------------------------------------------------
    Immediate application of nonstandard criterion for continuity can offer 

 by (auto_tac (claset(),simpset() addsimps [isNSCont_isCont_iff RS sym,
               isNSCont_minus]));
 qed "isCont_minus";
 
 Goalw [isCont_def]  
-      "[| isCont f x; f x \\<noteq> #0 |] ==> isCont (%x. inverse (f x)) x";
+      "[| isCont f x; f x \\<noteq> Numeral0 |] ==> isCont (%x. inverse (f x)) x";
 by (blast_tac (claset() addIs [LIM_inverse]) 1);
 qed "isCont_inverse";
 
-Goal "[| isNSCont f x; f x \\<noteq> #0 |] ==> isNSCont (%x. inverse (f x)) x";
+Goal "[| isNSCont f x; f x \\<noteq> Numeral0 |] ==> isNSCont (%x. inverse (f x)) x";
 by (auto_tac (claset() addIs [isCont_inverse],simpset() addsimps 
     [isNSCont_isCont_iff]));
 qed "isNSCont_inverse";
 
 Goalw [real_diff_def] 

 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 "\\<forall>s. #0 < s --> (\\<exists>z y. abs (z + - y) < s & r \\<le> abs (f z + -f y)) \
+Goal "\\<forall>s. Numeral0 < 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 \\<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 "\\<forall>s. #0 < s --> (\\<exists>z y. abs (z + - y) < s  & r \\<le> abs (f z + -f y)) \
+Goal "\\<forall>s. Numeral0 < 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 \\<le> abs(f (X n) + -f (Y n))";
 by (dtac lemma_LIMu 1);
 by (dtac choice 1);

 
 (*------------------------------------------------------------------
                          Derivatives
  ------------------------------------------------------------------*)
 Goalw [deriv_def] 
-      "(DERIV f x :> D) = ((%h. (f(x + h) + - f(x))/h) -- #0 --> D)";
+      "(DERIV f x :> D) = ((%h. (f(x + h) + - f(x))/h) -- Numeral0 --> D)";
 by (Blast_tac 1);        
 qed "DERIV_iff";
 
 Goalw [deriv_def] 
-      "(DERIV f x :> D) = ((%h. (f(x + h) + - f(x))/h) -- #0 --NS> D)";
+      "(DERIV f x :> D) = ((%h. (f(x + h) + - f(x))/h) -- Numeral0 --NS> D)";
 by (simp_tac (simpset() addsimps [LIM_NSLIM_iff]) 1);
 qed "DERIV_NS_iff";
 
 Goalw [deriv_def] 
       "DERIV f x :> D \
-\      ==> (%h. (f(x + h) + - f(x))/h) -- #0 --> D";
+\      ==> (%h. (f(x + h) + - f(x))/h) -- Numeral0 --> D";
 by (Blast_tac 1);        
 qed "DERIVD";
 
 Goalw [deriv_def] "DERIV f x :> D ==> \
-\          (%h. (f(x + h) + - f(x))/h) -- #0 --NS> D";
+\          (%h. (f(x + h) + - f(x))/h) -- Numeral0 --NS> D";
 by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff]) 1);
 qed "NS_DERIVD";
 
 (* Uniqueness *)
 Goalw [deriv_def] 

 (*--------------------------------------------------------
       Alternative definition for differentiability
  -------------------------------------------------------*)
 
 Goalw [LIM_def] 
- "((%h. (f(a + h) + - f(a))/h) -- #0 --> D) = \
+ "((%h. (f(a + h) + - f(a))/h) -- Numeral0 --> D) = \
 \ ((%x. (f(x) + -f(a)) / (x + -a)) -- a --> D)";
 by Safe_tac;
 by (ALLGOALS(dtac spec));
 by Safe_tac;
 by (Blast_tac 1 THEN Blast_tac 2);

    First NSDERIV in terms of NSLIM 
  -------------------------------------------*)
 
 (*--- first equivalence ---*)
 Goalw [nsderiv_def,NSLIM_def] 
-      "(NSDERIV f x :> D) = ((%h. (f(x + h) + - f(x))/h) -- #0 --NS> D)";
+      "(NSDERIV f x :> D) = ((%h. (f(x + h) + - f(x))/h) -- Numeral0 --NS> D)";
 by (auto_tac (claset(), simpset() addsimps [hypreal_of_real_zero]));
 by (dres_inst_tac [("x","xa")] bspec 1);
 by (rtac ccontr 3);
 by (dres_inst_tac [("x","h")] spec 3);
 by (auto_tac (claset(),

 (*-------------------------
     Constant function
  ------------------------*)
 
 (* use simple constant nslimit theorem *)
-Goal "(NSDERIV (%x. k) x :> #0)";
+Goal "(NSDERIV (%x. k) x :> Numeral0)";
 by (simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff]) 1);
 qed "NSDERIV_const";
 Addsimps [NSDERIV_const];
 
-Goal "(DERIV (%x. k) x :> #0)";
+Goal "(DERIV (%x. k) x :> Numeral0)";
 by (simp_tac (simpset() addsimps [NSDERIV_DERIV_iff RS sym]) 1);
 qed "DERIV_const";
 Addsimps [DERIV_const];
 
 (*-----------------------------------------------------

 by (simp_tac (simpset() addsimps [hypreal_add_mult_distrib2]) 1);
 val lemma_nsderiv1 = result();
 
 Goal "[| (x + y) / z = hypreal_of_real D + yb; z \\<noteq> 0; \
 \        z \\<in> Infinitesimal; yb \\<in> Infinitesimal |] \
-\     ==> x + y \\<approx> #0";
+\     ==> x + y \\<approx> Numeral0";
 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);
 by (auto_tac (claset() addSIs [Infinitesimal_HFinite_mult2, HFinite_add],
               simpset() addsimps [hypreal_mult_assoc, mem_infmal_iff RS sym]));

 \    -hypreal_of_real (f x)";
 by (etac (NSdifferentiableI RS incrementI) 1);
 qed "incrementI2";
 
 (* The Increment theorem -- Keisler p. 65 *)
-Goal "[| NSDERIV f x :> D; h \\<in> Infinitesimal; h \\<noteq> #0 |] \
+Goal "[| NSDERIV f x :> D; h \\<in> Infinitesimal; h \\<noteq> Numeral0 |] \
 \     ==> \\<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);
 by (forw_inst_tac [("b1","hypreal_of_real(D) + y")] 

              delsimps [hypreal_times_divide1_eq]) 1);
 by (auto_tac (claset(),
               simpset() addsimps [hypreal_add_mult_distrib]));
 qed "increment_thm";
 
-Goal "[| NSDERIV f x :> D; h \\<approx> #0; h \\<noteq> #0 |] \
+Goal "[| NSDERIV f x :> D; h \\<approx> Numeral0; h \\<noteq> Numeral0 |] \
 \     ==> \\<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 \\<approx> #0; h \\<noteq> #0 |] \
-\     ==> increment f x h \\<approx> #0";
+Goal "[| NSDERIV f x :> D; h \\<approx> Numeral0; h \\<noteq> Numeral0 |] \
+\     ==> increment f x h \\<approx> Numeral0";
 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]));
 by (etac (Infinitesimal_subset_HFinite RS subsetD) 1);
 qed "increment_approx_zero";

 (* lemmas *)
 Goalw [nsderiv_def] 
       "[| NSDERIV g x :> D; \
 \              (*f* g) (hypreal_of_real(x) + xa) = hypreal_of_real(g x);\
 \              xa \\<in> Infinitesimal;\
-\              xa \\<noteq> #0 \
-\           |] ==> D = #0";
+\              xa \\<noteq> Numeral0 \
+\           |] ==> D = Numeral0";
 by (dtac bspec 1);
 by Auto_tac;
 qed "NSDERIV_zero";
 
 (* can be proved differently using NSLIM_isCont_iff *)
 Goalw [nsderiv_def] 
-     "[| NSDERIV f x :> D;  h \\<in> Infinitesimal;  h \\<noteq> #0 |]  \
-\     ==> (*f* f) (hypreal_of_real(x) + h) + -hypreal_of_real(f x) \\<approx> #0";    
+     "[| NSDERIV f x :> D;  h \\<in> Infinitesimal;  h \\<noteq> Numeral0 |]  \
+\     ==> (*f* f) (hypreal_of_real(x) + h) + -hypreal_of_real(f x) \\<approx> Numeral0";    
 by (asm_full_simp_tac (simpset() addsimps 
     [mem_infmal_iff RS sym]) 1);
 by (rtac Infinitesimal_ratio 1);
 by (rtac approx_hypreal_of_real_HFinite 3);
 by Auto_tac;

 
                 f(x + h) - f(x)
                ----------------- \\<approx> Db
                        h
  --------------------------------------------------------------*)
-Goal "[| NSDERIV g x :> Db; xa \\<in> Infinitesimal; xa \\<noteq> #0 |] \
+Goal "[| NSDERIV g x :> Db; xa \\<in> Infinitesimal; xa \\<noteq> Numeral0 |] \
 \     ==> ((*f* g) (hypreal_of_real(x) + xa) + - hypreal_of_real(g x)) / xa \
 \         \\<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 "DERIV_chain2";
 
 (*------------------------------------------------------------------
            Differentiation of natural number powers
  ------------------------------------------------------------------*)
-Goal "NSDERIV (%x. x) x :> #1";
+Goal "NSDERIV (%x. x) x :> Numeral1";
 by (auto_tac (claset(),
      simpset() addsimps [NSDERIV_NSLIM_iff,
           NSLIM_def ,starfun_Id, hypreal_of_real_zero,
            hypreal_of_real_one]));
 qed "NSDERIV_Id";
 Addsimps [NSDERIV_Id];
 
 (*derivative of the identity function*)
-Goal "DERIV (%x. x) x :> #1";
+Goal "DERIV (%x. x) x :> Numeral1";
 by (simp_tac (simpset() addsimps [NSDERIV_DERIV_iff RS sym]) 1);
 qed "DERIV_Id";
 Addsimps [DERIV_Id];
 
 bind_thm ("isCont_Id", DERIV_Id RS DERIV_isCont);

 Goal "NSDERIV (op * c) x :> c";
 by (simp_tac (simpset() addsimps [NSDERIV_DERIV_iff]) 1);
 qed "NSDERIV_cmult_Id";
 Addsimps [NSDERIV_cmult_Id];
 
-Goal "DERIV (%x. x ^ n) x :> real n * (x ^ (n - 1'))";
+Goal "DERIV (%x. x ^ n) x :> real n * (x ^ (n - Suc 0))";
 by (induct_tac "n" 1);
 by (dtac (DERIV_Id RS DERIV_mult) 2);
 by (auto_tac (claset(), 
               simpset() addsimps [real_of_nat_Suc, real_add_mult_distrib]));
 by (case_tac "0 < n" 1);

 by (auto_tac (claset(), 
               simpset() addsimps [real_mult_assoc, real_add_commute]));
 qed "DERIV_pow";
 
 (* NS version *)
-Goal "NSDERIV (%x. x ^ n) x :> real n * (x ^ (n - 1'))";
+Goal "NSDERIV (%x. x ^ n) x :> real n * (x ^ (n - Suc 0))";
 by (simp_tac (simpset() addsimps [NSDERIV_DERIV_iff, DERIV_pow]) 1);
 qed "NSDERIV_pow";
 
 (*---------------------------------------------------------------
                     Power of -1 
  ---------------------------------------------------------------*)
 
-(*Can't get rid of x \\<noteq> #0 because it isn't continuous at zero*)
+(*Can't get rid of x \\<noteq> Numeral0 because it isn't continuous at zero*)
 Goalw [nsderiv_def]
-     "x \\<noteq> #0 ==> NSDERIV (%x. inverse(x)) x :> (- (inverse x ^ 2))";
+     "x \\<noteq> Numeral0 ==> NSDERIV (%x. inverse(x)) x :> (- (inverse x ^ Suc (Suc 0)))";
 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); 
 by (auto_tac (claset(),
      simpset() addsimps [starfun_inverse_inverse, realpow_two] 

 by (rtac Infinitesimal_HFinite_mult2 1); 
 by Auto_tac;  
 qed "NSDERIV_inverse";
 
 
-Goal "x \\<noteq> #0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ 2))";
+Goal "x \\<noteq> Numeral0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ Suc (Suc 0)))";
 by (asm_simp_tac (simpset() addsimps [NSDERIV_inverse,
          NSDERIV_DERIV_iff RS sym] delsimps [realpow_Suc]) 1);
 qed "DERIV_inverse";
 
 (*--------------------------------------------------------------
         Derivative of inverse 
  -------------------------------------------------------------*)
-Goal "[| DERIV f x :> d; f(x) \\<noteq> #0 |] \
-\     ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))";
+Goal "[| DERIV f x :> d; f(x) \\<noteq> Numeral0 |] \
+\     ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))";
 by (rtac (real_mult_commute RS subst) 1);
 by (asm_simp_tac (simpset() addsimps [real_minus_mult_eq1,
     realpow_inverse] delsimps [realpow_Suc, 
     real_minus_mult_eq1 RS sym]) 1);
 by (fold_goals_tac [o_def]);
 by (blast_tac (claset() addSIs [DERIV_chain,DERIV_inverse]) 1);
 qed "DERIV_inverse_fun";
 
-Goal "[| NSDERIV f x :> d; f(x) \\<noteq> #0 |] \
-\     ==> NSDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))";
+Goal "[| NSDERIV f x :> d; f(x) \\<noteq> Numeral0 |] \
+\     ==> NSDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))";
 by (asm_full_simp_tac (simpset() addsimps [NSDERIV_DERIV_iff,
             DERIV_inverse_fun] delsimps [realpow_Suc]) 1);
 qed "NSDERIV_inverse_fun";
 
 (*--------------------------------------------------------------
         Derivative of quotient 
  -------------------------------------------------------------*)
-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)";
+Goal "[| DERIV f x :> d; DERIV g x :> e; g(x) \\<noteq> Numeral0 |] \
+\      ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) + -(e*f(x))) / (g(x) ^ Suc (Suc 0))";
 by (dres_inst_tac [("f","g")] DERIV_inverse_fun 1);
 by (dtac DERIV_mult 2);
 by (REPEAT(assume_tac 1));
 by (asm_full_simp_tac
     (simpset() addsimps [real_divide_def, real_add_mult_distrib2,
                          realpow_inverse,real_minus_mult_eq1] @ real_mult_ac 
        delsimps [realpow_Suc, real_minus_mult_eq1 RS sym,
                  real_minus_mult_eq2 RS sym]) 1);
 qed "DERIV_quotient";
 
-Goal "[| NSDERIV f x :> d; DERIV g x :> e; g(x) \\<noteq> #0 |] \
+Goal "[| NSDERIV f x :> d; DERIV g x :> e; g(x) \\<noteq> Numeral0 |] \
 \      ==> NSDERIV (%y. f(y) / (g y)) x :> (d*g(x) \
-\                           + -(e*f(x))) / (g(x) ^ 2)";
+\                           + -(e*f(x))) / (g(x) ^ Suc (Suc 0))";
 by (asm_full_simp_tac (simpset() addsimps [NSDERIV_DERIV_iff,
             DERIV_quotient] delsimps [realpow_Suc]) 1);
 qed "NSDERIV_quotient";
  
 (* ------------------------------------------------------------------------ *)

 \     (\\<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 \\<noteq> x ==> z - x \\<noteq> (#0::real)"]));
+    ARITH_PROVE "z \\<noteq> x ==> z - x \\<noteq> (Numeral0::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";
 

 qed "lemma_nest";
 
 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 |] \
+\        (%n. f(n) - g(n)) ----> Numeral0 |] \
 \     ==> \\<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);

 by (induct_tac "n" 1);
 by (auto_tac (claset(), 
               simpset() addsimps [Bolzano_bisect_le, Let_def, split_def]));  
 qed "Bolzano_bisect_Suc_le_snd";
 
-Goal "((x::real) = y / (#2 * z)) = (#2 * x = y/z)";
+Goal "((x::real) = y / (# 2 * z)) = (# 2 * x = y/z)";
 by Auto_tac;  
-by (dres_inst_tac [("f","%u. (#1/#2)*u")] arg_cong 1); 
+by (dres_inst_tac [("f","%u. (Numeral1/# 2)*u")] arg_cong 1); 
 by Auto_tac;  
 qed "eq_divide_2_times_iff";
 
 Goal "a \\<le> b ==> \
 \     snd(Bolzano_bisect P a b n) - fst(Bolzano_bisect P a b n) = \
-\     (b-a) / (#2 ^ n)";
+\     (b-a) / (# 2 ^ n)";
 by (induct_tac "n" 1);
 by (auto_tac (claset(), 
       simpset() addsimps [eq_divide_2_times_iff, real_add_divide_distrib, 
                           Let_def, split_def]));
 by (auto_tac (claset(), 

 by (blast_tac (claset() addSEs [not_P_Bolzano_bisect RSN (2,rev_notE)]) 1); 
 qed "not_P_Bolzano_bisect'";
 
 
 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>x. \\<exists>d::real. Numeral0 < 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));

 by (dtac not_P_Bolzano_bisect' 1); 
 by (REPEAT (assume_tac 1));
 by (rename_tac "l" 1);
 by (dres_inst_tac [("x","l")] spec 1 THEN Clarify_tac 1);
 by (rewtac LIMSEQ_def);
-by (dres_inst_tac [("P", "%r. #0<r --> ?Q r"), ("x","d/#2")] spec 1);
-by (dres_inst_tac [("P", "%r. #0<r --> ?Q r"), ("x","d/#2")] spec 1);
+by (dres_inst_tac [("P", "%r. Numeral0<r --> ?Q r"), ("x","d/# 2")] spec 1);
+by (dres_inst_tac [("P", "%r. Numeral0<r --> ?Q r"), ("x","d/# 2")] spec 1);
 by (dtac real_less_half_sum 1);
 by Safe_tac;
 (*linear arithmetic bug if we just use Asm_simp_tac*)
 by (ALLGOALS Asm_full_simp_tac);
 by (dres_inst_tac [("x","fst(Bolzano_bisect P a b (no + noa))")] spec 1);

     (asm_full_simp_tac (simpset() addsimps [symmetric real_diff_def])));
 qed "lemma_BOLZANO";
 
 
 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>x. \\<exists>d::real. Numeral0 < 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";

 by (Blast_tac 2);
 by (asm_full_simp_tac (simpset() addsimps [isCont_iff,LIM_def]) 1);
 by (rtac ccontr 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 (dres_inst_tac [("P", "%d. Numeral0<d --> ?P d"),("x","Numeral1")] spec 2);
 by (Step_tac 2);
 by (Asm_full_simp_tac 2);
 by (Asm_full_simp_tac 2);
 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 --> (\\<exists>s. #0<s & ?Q r s)"),
+by (dres_inst_tac [("P", "%r. ?P r --> (\\<exists>s. Numeral0<s & ?Q r s)"),
                    ("x","abs(y - f x)")] spec 1);
 by Safe_tac;
 by (asm_full_simp_tac (simpset() addsimps []) 1);
 by (dres_inst_tac [("x","s")] spec 1);
 by (Clarify_tac 1);

 by (res_inst_tac [("x","M")] exI 1);
 by (Clarify_tac 1); 
 by (cut_inst_tac [("x","xb"),("y","xa")] linorder_linear 1);
 by (Force_tac 1); 
 by (case_tac "a \\<le> x & x \\<le> b" 1);
-by (res_inst_tac [("x","#1")] exI 2);
+by (res_inst_tac [("x","Numeral1")] 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 "\\<forall>M. \\<exists>x. a \\<le> x & x \\<le> b & ~ f x \\<le> M" 1);
-by (dres_inst_tac [("x","#1")] spec 1);
+by (dres_inst_tac [("x","Numeral1")] spec 1);
 by Auto_tac;  
 by (res_inst_tac [("x","s")] exI 1 THEN Clarify_tac 1);
-by (res_inst_tac [("x","abs(f x) + #1")] exI 1 THEN Clarify_tac 1);
+by (res_inst_tac [("x","abs(f x) + Numeral1")] exI 1 THEN Clarify_tac 1);
 by (dres_inst_tac [("x","xa - x")] spec 1 THEN Safe_tac);
 by (arith_tac 1);
 by (arith_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [abs_ge_self]) 1); 
 by (arith_tac 1);

 by (Blast_tac 2);
 by (subgoal_tac 
     "\\<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 "\\<forall>x. a \\<le> x & x \\<le> b --> #0 < inverse(M - f(x))" 1);
+by (subgoal_tac "\\<forall>x. a \\<le> x & x \\<le> b --> Numeral0 < 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 
-    "\\<forall>x. a \\<le> x & x \\<le> 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 + Numeral1)" 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 "\\<forall>x. a \\<le> x & x \\<le> b --> \
-\                inverse(k + #1) < inverse((%x. inverse(M - (f x))) x)" 1);
+\                inverse(k + Numeral1) < inverse((%x. inverse(M - (f x))) x)" 1);
 by Safe_tac;
 by (rtac real_inverse_less_swap 2);
 by (ALLGOALS Asm_full_simp_tac);
 by (dres_inst_tac [("P", "%N. N<M --> ?Q N"),
-                   ("x","M - inverse(k + #1)")] spec 1);
+                   ("x","M - inverse(k + Numeral1)")] spec 1);
 by (Step_tac 1 THEN dtac real_leI 1);
 by (dtac (real_le_diff_eq RS iffD1) 1);
 by (REPEAT(dres_inst_tac [("x","a")] spec 1));
 by (Asm_full_simp_tac 1);
 by (asm_full_simp_tac 

 (*----------------------------------------------------------------------------*)
 (* If f'(x) > 0 then x is locally strictly increasing at the right            *)
 (*----------------------------------------------------------------------------*)
 
 Goalw [deriv_def,LIM_def] 
-    "[| DERIV f x :> l;  #0 < l |] ==> \
-\      \\<exists>d. #0 < d & (\\<forall>h. #0 < h & h < d --> f(x) < f(x + h))";
+    "[| DERIV f x :> l;  Numeral0 < l |] ==> \
+\      \\<exists>d. Numeral0 < d & (\\<forall>h. Numeral0 < 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);
+by (subgoal_tac "Numeral0 < l*h" 1);
 by (asm_full_simp_tac (simpset() addsimps [real_0_less_mult_iff]) 2); 
 by (dres_inst_tac [("x","h")] spec 1);
 by (asm_full_simp_tac
     (simpset() addsimps [real_abs_def, real_inverse_eq_divide, 
                  pos_real_le_divide_eq, pos_real_less_divide_eq]
               addsplits [split_if_asm]) 1); 
 qed "DERIV_left_inc";
 
 Goalw [deriv_def,LIM_def] 
-    "[| DERIV f x :> l;  l < #0 |] ==> \
-\      \\<exists>d. #0 < d & (\\<forall>h. #0 < h & h < d --> f(x) < f(x - h))";
+    "[| DERIV f x :> l;  l < Numeral0 |] ==> \
+\      \\<exists>d. Numeral0 < d & (\\<forall>h. Numeral0 < 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);
+by (subgoal_tac "l*h < Numeral0" 1);
 by (asm_full_simp_tac (simpset() addsimps [real_mult_less_0_iff]) 2); 
 by (dres_inst_tac [("x","-h")] spec 1);
 by (asm_full_simp_tac
     (simpset() addsimps [real_abs_def, real_inverse_eq_divide, 
                          pos_real_less_divide_eq,
                          symmetric real_diff_def]
                addsplits [split_if_asm]) 1);
-by (subgoal_tac "#0 < (f (x - h) - f x)/h" 1);
+by (subgoal_tac "Numeral0 < (f (x - h) - f x)/h" 1);
 by (arith_tac 2);
 by (asm_full_simp_tac
     (simpset() addsimps [pos_real_less_divide_eq]) 1); 
 qed "DERIV_left_dec";
 
 
 Goal "[| DERIV f x :> l; \
-\        \\<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);
+\        \\<exists>d. Numeral0 < d & (\\<forall>y. abs(x - y) < d --> f(y) \\<le> f(x)) |] \
+\     ==> l = Numeral0";
+by (res_inst_tac [("R1.0","l"),("R2.0","Numeral0")] real_linear_less2 1);
 by Safe_tac;
 by (dtac DERIV_left_dec 1);
 by (dtac DERIV_left_inc 3);
 by Safe_tac;
 by (dres_inst_tac [("d1.0","d"),("d2.0","da")] real_lbound_gt_zero 1);

 (*----------------------------------------------------------------------------*)
 (* Similar theorem for a local minimum                                        *)
 (*----------------------------------------------------------------------------*)
 
 Goal "[| DERIV f x :> l; \
-\        \\<exists>d::real. #0 < d & (\\<forall>y. abs(x - y) < d --> f(x) \\<le> f(y)) |] \
-\     ==> l = #0";
+\        \\<exists>d::real. Numeral0 < d & (\\<forall>y. abs(x - y) < d --> f(x) \\<le> f(y)) |] \
+\     ==> l = Numeral0";
 by (dtac (DERIV_minus RS DERIV_local_max) 1); 
 by Auto_tac;  
 qed "DERIV_local_min";
 
 (*----------------------------------------------------------------------------*)
 (* In particular if a function is locally flat                                *)
 (*----------------------------------------------------------------------------*)
 
 Goal "[| DERIV f x :> l; \
-\        \\<exists>d. #0 < d & (\\<forall>y. abs(x - y) < d --> f(x) = f(y)) |] \
-\     ==> l = #0";
+\        \\<exists>d. Numeral0 < d & (\\<forall>y. abs(x - y) < d --> f(x) = f(y)) |] \
+\     ==> l = Numeral0";
 by (auto_tac (claset() addSDs [DERIV_local_max],simpset()));
 qed "DERIV_local_const";
 
 (*----------------------------------------------------------------------------*)
 (* Lemma about introducing open ball in open interval                         *)
 (*----------------------------------------------------------------------------*)
 
 Goal "[| a < x;  x < b |] ==> \
-\       \\<exists>d::real. #0 < d &  (\\<forall>y. abs(x - y) < d --> a < y & y < b)";
+\       \\<exists>d::real. Numeral0 < 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;
 by (res_inst_tac [("x","x - a")] exI 1);
 by (res_inst_tac [("x","b - x")] exI 2);
 by Auto_tac;
 by (auto_tac (claset(),simpset() addsimps [real_less_diff_eq]));
 qed "lemma_interval_lt";
 
 Goal "[| a < x;  x < b |] ==> \
-\       \\<exists>d::real. #0 < d &  (\\<forall>y. abs(x - y) < d --> a \\<le> y & y \\<le> b)";
+\       \\<exists>d::real. Numeral0 < 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()));
 qed "lemma_interval";
 
 (*-----------------------------------------------------------------------
             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 \\<in> (a,b) such that f'(x0) = #0
+   then x0 \\<in> (a,b) such that f'(x0) = Numeral0
  ----------------------------------------------------------------------*)
 
 Goal "[| a < b; f(a) = f(b); \
 \        \\<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";
+\     |] ==> \\<exists>z. a < z & z < b & DERIV f z :> Numeral0";
 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);
 by (EVERY1[assume_tac,Step_tac]);
 by (case_tac "a < x & x < b" 1 THEN etac conjE 1);
 by (Asm_full_simp_tac 2);
 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 "(\\<exists>l. DERIV f x :> l) & \
-\        (\\<exists>d. #0 < d & (\\<forall>y. abs(x - y) < d --> f(y) \\<le> f(x)))" 1);
+\        (\\<exists>d. Numeral0 < 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);
 by (ftac DERIV_local_max 1);
 by (EVERY1[Blast_tac,Blast_tac]);

 by (Asm_full_simp_tac 2);
 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 "(\\<exists>l. DERIV f xa :> l) & \
-\        (\\<exists>d. #0 < d & (\\<forall>y. abs(xa - y) < d --> f(xa) \\<le> f(y)))" 1);
+\        (\\<exists>d. Numeral0 < 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 (res_inst_tac [("x","r")] exI 1 THEN Asm_full_simp_tac 1);
 by (etac conjE 1);
 by (forw_inst_tac [("a","a"),("x","r")] lemma_interval 1);
 by (EVERY1[assume_tac, etac exE]);
 by (subgoal_tac "(\\<exists>l. DERIV f r :> l) & \
-\        (\\<exists>d. #0 < d & (\\<forall>y. abs(r - y) < d --> f(r) = f(y)))" 1);
+\        (\\<exists>d. Numeral0 < 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]);
 by (res_inst_tac [("x","d")] exI 1);
 by (EVERY1[rtac conjI, Blast_tac, rtac allI, rtac impI]);

 (* Theorem that function is constant if its derivative is 0 over an interval. *)
 (*----------------------------------------------------------------------------*)
 
 Goal "[| a < b; \
 \        \\<forall>x. a \\<le> x & x \\<le> b --> isCont f x; \
-\        \\<forall>x. a < x & x < b --> DERIV f x :> #0 |] \
+\        \\<forall>x. a < x & x < b --> DERIV f x :> Numeral0 |] \
 \       ==> (f b = f a)";
 by (dtac MVT 1 THEN assume_tac 1);
 by (blast_tac (claset() addIs [differentiableI]) 1);
 by (auto_tac (claset() addSDs [DERIV_unique],simpset() 
     addsimps [real_diff_eq_eq]));
 qed "DERIV_isconst_end";
 
 Goal "[| a < b; \
 \        \\<forall>x. a \\<le> x & x \\<le> b --> isCont f x; \
-\        \\<forall>x. a < x & x < b --> DERIV f x :> #0 |] \
+\        \\<forall>x. a < x & x < b --> DERIV f x :> Numeral0 |] \
 \       ==> \\<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;
 by (dres_inst_tac [("b","x")] DERIV_isconst_end 1);
 by Auto_tac;
 qed "DERIV_isconst1";
 
 Goal "[| a < b; \
 \        \\<forall>x. a \\<le> x & x \\<le> b --> isCont f x; \
-\        \\<forall>x. a < x & x < b --> DERIV f x :> #0; \
+\        \\<forall>x. a < x & x < b --> DERIV f x :> Numeral0; \
 \        a \\<le> x; x \\<le> b |] \
 \       ==> f x = f a";
 by (blast_tac (claset() addDs [DERIV_isconst1]) 1);
 qed "DERIV_isconst2";
 
-Goal "\\<forall>x. DERIV f x :> #0 ==> f(x) = f(y)";
+Goal "\\<forall>x. DERIV f x :> Numeral0 ==> 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";
 

 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]));
 qed "DERIV_const_ratio_const2";
 
-Goal "((a + b) /#2 - a) = (b - a)/(#2::real)";
+Goal "((a + b) /# 2 - a) = (b - a)/(# 2::real)";
 by Auto_tac;  
 qed "real_average_minus_first";
 Addsimps [real_average_minus_first];
 
-Goal "((b + a)/#2 - a) = (b - a)/(#2::real)";
+Goal "((b + a)/# 2 - a) = (b - a)/(# 2::real)";
 by Auto_tac;  
 qed "real_average_minus_second";
 Addsimps [real_average_minus_second];
 
 
 (* Gallileo's "trick": average velocity = av. of end velocities *)
 Goal "[|a \\<noteq> (b::real); \\<forall>x. DERIV v x :> k|] \
-\     ==> v((a + b)/#2) = (v a + v b)/#2";
+\     ==> 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;
 by (ftac DERIV_const_ratio_const2 1 THEN assume_tac 1);
 by (ftac DERIV_const_ratio_const2 2 THEN assume_tac 2);
 by (dtac real_less_half_sum 1);

 (* ------------------------------------------------------------------------ *)
 (* Dull lemma that an continuous injection on an interval must have a strict*)
 (* maximum at an end point, not in the middle.                              *)
 (* ------------------------------------------------------------------------ *)
 
-Goal "[|#0 < d; \\<forall>z. abs(z - x) \\<le> d --> g(f z) = z; \
+Goal "[|Numeral0 < 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);

 
 (* ------------------------------------------------------------------------ *)
 (* Similar version for lower bound                                          *)
 (* ------------------------------------------------------------------------ *)
 
-Goal "[|#0 < d; \\<forall>z. abs(z - x) \\<le> d --> g(f z) = z; \
+Goal "[|Numeral0 < 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]));

 (* Also from John's theory                                                  *)
 (* ------------------------------------------------------------------------ *)
 
 Addsimps [zero_eq_numeral_0,one_eq_numeral_1];
 
-val lemma_le = ARITH_PROVE "#0 \\<le> (d::real) ==> -d \\<le> d";
+val lemma_le = ARITH_PROVE "Numeral0 \\<le> (d::real) ==> -d \\<le> d";
 
 (* FIXME: awful proof - needs improvement *)
-Goal "[| #0 < d; \\<forall>z. abs(z - x) \\<le> d --> g(f z) = z; \
+Goal "[| Numeral0 < 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 & \
+\      ==> \\<exists>e. Numeral0 < 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 

 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);
 by Safe_tac;
-by (dres_inst_tac [("x","L")] (ARITH_PROVE "x < y ==> #0 < y - (x::real)") 1);
-by (dres_inst_tac [("x","f x")] (ARITH_PROVE "x < y ==> #0 < y - (x::real)") 1);
+by (dres_inst_tac [("x","L")] (ARITH_PROVE "x < y ==> Numeral0 < y - (x::real)") 1);
+by (dres_inst_tac [("x","f x")] (ARITH_PROVE "x < y ==> Numeral0 < y - (x::real)") 1);
 by (dres_inst_tac [("d1.0","f x - L"),("d2.0","M - f x")] 
     (rename_numerals real_lbound_gt_zero) 1);
 by Safe_tac;
 by (res_inst_tac [("x","e")] exI 1);
 by Safe_tac;

 
 (* ------------------------------------------------------------------------ *)
 (* Continuity of inverse function                                           *)
 (* ------------------------------------------------------------------------ *)
 
-Goal "[| #0 < d; \\<forall>z. abs(z - x) \\<le> d --> g(f(z)) = z; \
+Goal "[| Numeral0 < 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);