diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/Hyperreal/Lim.ML
--- a/src/HOL/Hyperreal/Lim.ML	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Hyperreal/Lim.ML	Sat Oct 06 00:02:46 2001 +0200
@@ -29,7 +29,7 @@
 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")] 
@@ -1544,15 +1544,15 @@
               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. (Numeral1/# 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, 
@@ -1604,8 +1604,8 @@
 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. 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 (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*)
@@ -2148,12 +2148,12 @@
               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];
@@ -2161,7 +2161,7 @@
 
 (* 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);