# HG changeset patch
# User wenzelm
# Date 1002319366 -7200
# Node ID 3c50a2cd6f00e303d92da90d0213ace3d376cad2
# Parent  6e5de8d4290a2b4ef96e50630dedcf9d00b237d8
* sane numerals (stage 2): plain "num" syntax (removed "#");

diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/Algebra/poly/PolyHomo.ML
--- a/src/HOL/Algebra/poly/PolyHomo.ML	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Algebra/poly/PolyHomo.ML	Sat Oct 06 00:02:46 2001 +0200
@@ -112,15 +112,15 @@
 (* Examples *)
 
 Goal
-  "EVAL (x::'a::domain) (a*X^# 2 + b*X^1 + c*X^0) = a * x ^ # 2 + b * x ^ 1 + c";
+  "EVAL (x::'a::domain) (a*X^2 + b*X^1 + c*X^0) = a * x ^ 2 + b * x ^ 1 + c";
 by (asm_simp_tac (simpset() delsimps [power_Suc]
     addsimps [EVAL_homo, EVAL_monom, EVAL_smult]) 1);
 result();
 
 Goal
   "EVAL (y::'a::domain) \
-\    (EVAL (const x) (monom 1 + const (a*X^# 2 + b*X^1 + c*X^0))) = \
-\  x ^ 1 + (a * y ^ # 2 + b * y ^ 1 + c)";
+\    (EVAL (const x) (monom 1 + const (a*X^2 + b*X^1 + c*X^0))) = \
+\  x ^ 1 + (a * y ^ 2 + b * y ^ 1 + c)";
 by (asm_simp_tac (simpset() delsimps [power_Suc]
     addsimps [EVAL_homo, EVAL_monom, EVAL_smult, EVAL_const]) 1);
 result();
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/Auth/KerberosIV.thy
--- a/src/HOL/Auth/KerberosIV.thy	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Auth/KerberosIV.thy	Sat Oct 06 00:02:46 2001 +0200
@@ -65,8 +65,8 @@
     RespLife   :: nat 
 
 rules
-     AuthLife_LB    "# 2 <= AuthLife"
-     ServLife_LB    "# 2 <= ServLife"
+     AuthLife_LB    "2 <= AuthLife"
+     ServLife_LB    "2 <= ServLife"
      AutcLife_LB    "Suc 0 <= AutcLife" 
      RespLife_LB    "Suc 0 <= RespLife"
 
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/Auth/Kerberos_BAN.thy
--- a/src/HOL/Auth/Kerberos_BAN.thy	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Auth/Kerberos_BAN.thy	Sat Oct 06 00:02:46 2001 +0200
@@ -30,7 +30,7 @@
 
 rules
     (*The ticket should remain fresh for two journeys on the network at least*)
-    SesKeyLife_LB "# 2 <= SesKeyLife"
+    SesKeyLife_LB "2 <= SesKeyLife"
 
     (*The authenticator only for one journey*)
     AutLife_LB    "Suc 0 <= AutLife"
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/GroupTheory/Exponent.ML
--- a/src/HOL/GroupTheory/Exponent.ML	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/GroupTheory/Exponent.ML	Sat Oct 06 00:02:46 2001 +0200
@@ -205,13 +205,13 @@
 by (induct_tac "n" 1);
 by (Asm_simp_tac 1); 
 by (Asm_full_simp_tac 1); 
-by (subgoal_tac "# 2 * n + # 2 <= p * p^n" 1);
+by (subgoal_tac "2 * n + 2 <= p * p^n" 1);
 by (Asm_full_simp_tac 1); 
-by (subgoal_tac "# 2 * p^n <= p * p^n" 1);
+by (subgoal_tac "2 * p^n <= p * p^n" 1);
 (*?arith_tac should handle all of this!*)
 by (rtac order_trans 1); 
 by (assume_tac 2); 
-by (dres_inst_tac [("k","# 2")] mult_le_mono2 1); 
+by (dres_inst_tac [("k","2")] mult_le_mono2 1); 
 by (Asm_full_simp_tac 1); 
 by (rtac mult_le_mono1 1); 
 by (Asm_full_simp_tac 1); 
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/Hoare/Arith2.ML
--- a/src/HOL/Hoare/Arith2.ML	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Hoare/Arith2.ML	Sat Oct 06 00:02:46 2001 +0200
@@ -63,7 +63,7 @@
 
 (*** pow ***)
 
-Goal "m mod # 2 = 0 ==> ((n::nat)*n)^(m div # 2) = n^m";
+Goal "m mod 2 = 0 ==> ((n::nat)*n)^(m div 2) = n^m";
 by (asm_simp_tac (simpset() addsimps [power_two RS sym, power_mult RS sym,
 				      mult_div_cancel]) 1);
 qed "sq_pow_div2";
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/Hoare/Examples.ML
--- a/src/HOL/Hoare/Examples.ML	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Hoare/Examples.ML	Sat Oct 06 00:02:46 2001 +0200
@@ -50,9 +50,9 @@
 Goal "|- VARS a b x y. \
 \ {0<A & 0<B & a=A & b=B & x=B & y=A} \
 \ WHILE  a ~= b  \
-\ INV {0<a & 0<b & gcd A B = gcd a b & # 2*A*B = a*x + b*y} \
+\ INV {0<a & 0<b & gcd A B = gcd a b & 2*A*B = a*x + b*y} \
 \ DO IF a<b THEN (b := b-a; x := x+y) ELSE (a := a-b; y := y+x) FI OD \
-\ {a = gcd A B & # 2*A*B = a*(x+y)}";
+\ {a = gcd A B & 2*A*B = a*(x+y)}";
 by (hoare_tac (K all_tac) 1);
 by(Asm_simp_tac 1);
 by(asm_simp_tac (simpset() addsimps
@@ -68,9 +68,9 @@
 \ c := (1::nat); \
 \ WHILE b ~= 0 \
 \ INV {A^B = c * a^b} \
-\ DO  WHILE b mod # 2 = 0 \
+\ DO  WHILE b mod 2 = 0 \
 \     INV {A^B = c * a^b} \
-\     DO  a := a*a; b := b div # 2 OD; \
+\     DO  a := a*a; b := b div 2 OD; \
 \     c := c*a; b := b - 1 \
 \ OD \
 \ {c = A^B}";
@@ -114,7 +114,7 @@
 \ x := X; u := 1; w := 1; r := (0::nat); \
 \ WHILE w <= x \
 \ INV {u = r+r+1 & w = (r+1)*(r+1) & r*r <= x & x=X} \
-\ DO r := r + 1; w := w + u + # 2; u := u + # 2 OD \
+\ DO r := r + 1; w := w + u + 2; u := u + 2 OD \
 \ {r*r <= X & X < (r+1)*(r+1)}";
 by (hoare_tac (SELECT_GOAL Auto_tac) 1);
 qed "sqrt_without_multiplication";
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/Hyperreal/HyperArith0.ML
--- a/src/HOL/Hyperreal/HyperArith0.ML	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Hyperreal/HyperArith0.ML	Sat Oct 06 00:02:46 2001 +0200
@@ -288,34 +288,34 @@
 set trace_simp;
 fun test s = (Goal s; by (Simp_tac 1)); 
 
-test "Numeral0 <= (y::hypreal) * # -2";
-test "# 9*x = # 12 * (y::hypreal)";
-test "(# 9*x) / (# 12 * (y::hypreal)) = z";
-test "# 9*x < # 12 * (y::hypreal)";
-test "# 9*x <= # 12 * (y::hypreal)";
+test "Numeral0 <= (y::hypreal) * -2";
+test "9*x = 12 * (y::hypreal)";
+test "(9*x) / (12 * (y::hypreal)) = z";
+test "9*x < 12 * (y::hypreal)";
+test "9*x <= 12 * (y::hypreal)";
 
-test "# -99*x = # 123 * (y::hypreal)";
-test "(# -99*x) / (# 123 * (y::hypreal)) = z";
-test "# -99*x < # 123 * (y::hypreal)";
-test "# -99*x <= # 123 * (y::hypreal)";
+test "-99*x = 123 * (y::hypreal)";
+test "(-99*x) / (123 * (y::hypreal)) = z";
+test "-99*x < 123 * (y::hypreal)";
+test "-99*x <= 123 * (y::hypreal)";
 
-test "# 999*x = # -396 * (y::hypreal)";
-test "(# 999*x) / (# -396 * (y::hypreal)) = z";
-test "# 999*x < # -396 * (y::hypreal)";
-test "# 999*x <= # -396 * (y::hypreal)";
+test "999*x = -396 * (y::hypreal)";
+test "(999*x) / (-396 * (y::hypreal)) = z";
+test "999*x < -396 * (y::hypreal)";
+test "999*x <= -396 * (y::hypreal)";
 
-test "# -99*x = # -81 * (y::hypreal)";
-test "(# -99*x) / (# -81 * (y::hypreal)) = z";
-test "# -99*x <= # -81 * (y::hypreal)";
-test "# -99*x < # -81 * (y::hypreal)";
+test "-99*x = -81 * (y::hypreal)";
+test "(-99*x) / (-81 * (y::hypreal)) = z";
+test "-99*x <= -81 * (y::hypreal)";
+test "-99*x < -81 * (y::hypreal)";
 
-test "# -2 * x = # -1 * (y::hypreal)";
-test "# -2 * x = -(y::hypreal)";
-test "(# -2 * x) / (# -1 * (y::hypreal)) = z";
-test "# -2 * x < -(y::hypreal)";
-test "# -2 * x <= # -1 * (y::hypreal)";
-test "-x < # -23 * (y::hypreal)";
-test "-x <= # -23 * (y::hypreal)";
+test "-2 * x = -1 * (y::hypreal)";
+test "-2 * x = -(y::hypreal)";
+test "(-2 * x) / (-1 * (y::hypreal)) = z";
+test "-2 * x < -(y::hypreal)";
+test "-2 * x <= -1 * (y::hypreal)";
+test "-x < -23 * (y::hypreal)";
+test "-x <= -23 * (y::hypreal)";
 *)
 
 
@@ -516,18 +516,18 @@
 qed "hypreal_divide_1";
 Addsimps [hypreal_divide_1];
 
-Goal "x/# -1 = -(x::hypreal)";
+Goal "x/-1 = -(x::hypreal)";
 by (Simp_tac 1); 
 qed "hypreal_divide_minus1";
 Addsimps [hypreal_divide_minus1];
 
-Goal "# -1/(x::hypreal) = - (Numeral1/x)";
+Goal "-1/(x::hypreal) = - (Numeral1/x)";
 by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_minus_inverse]) 1); 
 qed "hypreal_minus1_divide";
 Addsimps [hypreal_minus1_divide];
 
 Goal "[| (Numeral0::hypreal) < d1; Numeral0 < d2 |] ==> EX e. Numeral0 < e & e < d1 & e < d2";
-by (res_inst_tac [("x","(min d1 d2)/# 2")] exI 1); 
+by (res_inst_tac [("x","(min d1 d2)/2")] exI 1); 
 by (asm_simp_tac (simpset() addsimps [min_def]) 1); 
 qed "hypreal_lbound_gt_zero";
 
@@ -644,11 +644,11 @@
 
 (*** Density of the Hyperreals ***)
 
-Goal "x < y ==> x < (x+y) / (# 2::hypreal)";
+Goal "x < y ==> x < (x+y) / (2::hypreal)";
 by Auto_tac;
 qed "hypreal_less_half_sum";
 
-Goal "x < y ==> (x+y)/(# 2::hypreal) < y";
+Goal "x < y ==> (x+y)/(2::hypreal) < y";
 by Auto_tac;
 qed "hypreal_gt_half_sum";
 
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/Hyperreal/HyperBin.ML
--- a/src/HOL/Hyperreal/HyperBin.ML	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Hyperreal/HyperBin.ML	Sat Oct 06 00:02:46 2001 +0200
@@ -57,18 +57,18 @@
 qed "mult_hypreal_number_of";
 Addsimps [mult_hypreal_number_of];
 
-Goal "(# 2::hypreal) = Numeral1 + Numeral1";
+Goal "(2::hypreal) = Numeral1 + Numeral1";
 by (Simp_tac 1);
 val lemma = result();
 
 (*For specialist use: NOT as default simprules*)
-Goal "# 2 * z = (z+z::hypreal)";
+Goal "2 * z = (z+z::hypreal)";
 by (simp_tac (simpset ()
 	      addsimps [lemma, hypreal_add_mult_distrib,
 			one_eq_numeral_1 RS sym]) 1);
 qed "hypreal_mult_2";
 
-Goal "z * # 2 = (z+z::hypreal)";
+Goal "z * 2 = (z+z::hypreal)";
 by (stac hypreal_mult_commute 1 THEN rtac hypreal_mult_2 1);
 qed "hypreal_mult_2_right";
 
@@ -107,11 +107,11 @@
 
 (*** New versions of existing theorems involving 0, 1hr ***)
 
-Goal "- Numeral1 = (# -1::hypreal)";
+Goal "- Numeral1 = (-1::hypreal)";
 by (Simp_tac 1);
 qed "minus_numeral_one";
 
-(*Maps 0 to Numeral0 and 1hr to Numeral1 and -1hr to # -1*)
+(*Maps 0 to Numeral0 and 1hr to Numeral1 and -1hr to -1*)
 val hypreal_numeral_ss = 
     real_numeral_ss addsimps [zero_eq_numeral_0, one_eq_numeral_1, 
 		              minus_numeral_one];
@@ -242,14 +242,14 @@
                         hypreal_add_ac@rel_iff_rel_0_rls) 1);
 qed "hypreal_le_add_iff2";
 
-Goal "(z::hypreal) * # -1 = -z";
+Goal "(z::hypreal) * -1 = -z";
 by (stac (minus_numeral_one RS sym) 1);
 by (stac (hypreal_minus_mult_eq2 RS sym) 1); 
 by Auto_tac;  
 qed "hypreal_mult_minus_1_right";
 Addsimps [hypreal_mult_minus_1_right];
 
-Goal "# -1 * (z::hypreal) = -z";
+Goal "-1 * (z::hypreal) = -z";
 by (simp_tac (simpset() addsimps [hypreal_mult_commute]) 1); 
 qed "hypreal_mult_minus_1";
 Addsimps [hypreal_mult_minus_1];
@@ -471,7 +471,7 @@
 structure CombineNumeralsData =
   struct
   val add		= op + : int*int -> int 
-  val mk_sum    	= long_mk_sum    (*to work for e.g. # 2*x + # 3*x *)
+  val mk_sum    	= long_mk_sum    (*to work for e.g. 2*x + 3*x *)
   val dest_sum		= dest_sum
   val mk_coeff		= mk_coeff
   val dest_coeff	= dest_coeff 1
@@ -530,34 +530,34 @@
 set trace_simp;
 fun test s = (Goal s, by (Simp_tac 1)); 
 
-test "l + # 2 + # 2 + # 2 + (l + # 2) + (oo + # 2) = (uu::hypreal)";
-test "# 2*u = (u::hypreal)";
-test "(i + j + # 12 + (k::hypreal)) - # 15 = y";
-test "(i + j + # 12 + (k::hypreal)) - # 5 = y";
+test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::hypreal)";
+test "2*u = (u::hypreal)";
+test "(i + j + 12 + (k::hypreal)) - 15 = y";
+test "(i + j + 12 + (k::hypreal)) - 5 = y";
 
 test "y - b < (b::hypreal)";
-test "y - (# 3*b + c) < (b::hypreal) - # 2*c";
+test "y - (3*b + c) < (b::hypreal) - 2*c";
 
-test "(# 2*x - (u*v) + y) - v*# 3*u = (w::hypreal)";
-test "(# 2*x*u*v + (u*v)*# 4 + y) - v*u*# 4 = (w::hypreal)";
-test "(# 2*x*u*v + (u*v)*# 4 + y) - v*u = (w::hypreal)";
-test "u*v - (x*u*v + (u*v)*# 4 + y) = (w::hypreal)";
+test "(2*x - (u*v) + y) - v*3*u = (w::hypreal)";
+test "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::hypreal)";
+test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::hypreal)";
+test "u*v - (x*u*v + (u*v)*4 + y) = (w::hypreal)";
 
-test "(i + j + # 12 + (k::hypreal)) = u + # 15 + y";
-test "(i + j*# 2 + # 12 + (k::hypreal)) = j + # 5 + y";
+test "(i + j + 12 + (k::hypreal)) = u + 15 + y";
+test "(i + j*2 + 12 + (k::hypreal)) = j + 5 + y";
 
-test "# 2*y + # 3*z + # 6*w + # 2*y + # 3*z + # 2*u = # 2*y' + # 3*z' + # 6*w' + # 2*y' + # 3*z' + u + (vv::hypreal)";
+test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + (vv::hypreal)";
 
 test "a + -(b+c) + b = (d::hypreal)";
 test "a + -(b+c) - b = (d::hypreal)";
 
 (*negative numerals*)
-test "(i + j + # -2 + (k::hypreal)) - (u + # 5 + y) = zz";
-test "(i + j + # -3 + (k::hypreal)) < u + # 5 + y";
-test "(i + j + # 3 + (k::hypreal)) < u + # -6 + y";
-test "(i + j + # -12 + (k::hypreal)) - # 15 = y";
-test "(i + j + # 12 + (k::hypreal)) - # -15 = y";
-test "(i + j + # -12 + (k::hypreal)) - # -15 = y";
+test "(i + j + -2 + (k::hypreal)) - (u + 5 + y) = zz";
+test "(i + j + -3 + (k::hypreal)) < u + 5 + y";
+test "(i + j + 3 + (k::hypreal)) < u + -6 + y";
+test "(i + j + -12 + (k::hypreal)) - 15 = y";
+test "(i + j + 12 + (k::hypreal)) - -15 = y";
+test "(i + j + -12 + (k::hypreal)) - -15 = y";
 *)
 
 
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/Hyperreal/HyperPow.ML
--- a/src/HOL/Hyperreal/HyperPow.ML	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Hyperreal/HyperPow.ML	Sat Oct 06 00:02:46 2001 +0200
@@ -75,7 +75,7 @@
 qed "hrabs_minus_hrealpow_one";
 Addsimps [hrabs_minus_hrealpow_one];
 
-Goal "abs(# -1 ^ n) = (Numeral1::hypreal)";
+Goal "abs(-1 ^ n) = (Numeral1::hypreal)";
 by (induct_tac "n" 1);
 by Auto_tac;  
 qed "hrabs_hrealpow_minus_one";
@@ -134,13 +134,13 @@
 by Auto_tac;  
 qed "hrealpow_two_ge_one";
 
-Goal "(Numeral1::hypreal) <= # 2 ^ n";
+Goal "(Numeral1::hypreal) <= 2 ^ n";
 by (res_inst_tac [("y","Numeral1 ^ n")] order_trans 1);
 by (rtac hrealpow_le 2);
 by Auto_tac;
 qed "two_hrealpow_ge_one";
 
-Goal "hypreal_of_nat n < # 2 ^ n";
+Goal "hypreal_of_nat n < 2 ^ n";
 by (induct_tac "n" 1);
 by (auto_tac (claset(),
         simpset() addsimps [hypreal_of_nat_Suc, hypreal_add_mult_distrib]));
@@ -149,17 +149,17 @@
 qed "two_hrealpow_gt";
 Addsimps [two_hrealpow_gt,two_hrealpow_ge_one];
 
-Goal "# -1 ^ (# 2*n) = (Numeral1::hypreal)";
+Goal "-1 ^ (2*n) = (Numeral1::hypreal)";
 by (induct_tac "n" 1);
 by (Auto_tac);
 qed "hrealpow_minus_one";
 
-Goal "n+n = (# 2*n::nat)";
+Goal "n+n = (2*n::nat)";
 by Auto_tac; 
 qed "double_lemma";
 
 (*ugh: need to get rid fo the n+n*)
-Goal "# -1 ^ (n + n) = (Numeral1::hypreal)";
+Goal "-1 ^ (n + n) = (Numeral1::hypreal)";
 by (auto_tac (claset(), 
               simpset() addsimps [double_lemma, hrealpow_minus_one]));
 qed "hrealpow_minus_one2";
@@ -340,7 +340,7 @@
 qed "hrabs_minus_hyperpow_one";
 Addsimps [hrabs_minus_hyperpow_one];
 
-Goal "abs(# -1 pow n) = (Numeral1::hypreal)";
+Goal "abs(-1 pow n) = (Numeral1::hypreal)";
 by (subgoal_tac "abs((- 1hr) pow n) = 1hr" 1);
 by (Asm_full_simp_tac 1); 
 by (simp_tac (HOL_ss addsimps [hypreal_one_def]) 1);
@@ -388,7 +388,7 @@
               simpset()));
 qed "hyperpow_two_ge_one";
 
-Goal "(Numeral1::hypreal) <= # 2 pow n";
+Goal "(Numeral1::hypreal) <= 2 pow n";
 by (res_inst_tac [("y","Numeral1 pow n")] order_trans 1);
 by (rtac hyperpow_le 2);
 by Auto_tac;
@@ -397,7 +397,7 @@
 
 Addsimps [simplify (simpset()) realpow_minus_one];
 
-Goal "# -1 pow ((1hn + 1hn)*n) = (Numeral1::hypreal)";
+Goal "-1 pow ((1hn + 1hn)*n) = (Numeral1::hypreal)";
 by (subgoal_tac "(-(1hr)) pow ((1hn + 1hn)*n) = 1hr" 1);
 by (Asm_full_simp_tac 1); 
 by (simp_tac (HOL_ss addsimps [hypreal_one_def]) 1);
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);
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/Hyperreal/Lim.thy
--- a/src/HOL/Hyperreal/Lim.thy	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Hyperreal/Lim.thy	Sat Oct 06 00:02:46 2001 +0200
@@ -71,8 +71,8 @@
   "Bolzano_bisect P a b 0 = (a,b)"
   "Bolzano_bisect P a b (Suc n) =
       (let (x,y) = Bolzano_bisect P a b n
-       in if P(x, (x+y)/# 2) then ((x+y)/# 2, y)
-                            else (x, (x+y)/# 2) )"
+       in if P(x, (x+y)/2) then ((x+y)/2, y)
+                            else (x, (x+y)/2) )"
   
 
 end
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/Hyperreal/NSA.ML
--- a/src/HOL/Hyperreal/NSA.ML	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Hyperreal/NSA.ML	Sat Oct 06 00:02:46 2001 +0200
@@ -260,11 +260,11 @@
 qed "Infinitesimal_zero";
 AddIffs [Infinitesimal_zero];
 
-Goal "x/(# 2::hypreal) + x/(# 2::hypreal) = x";
+Goal "x/(2::hypreal) + x/(2::hypreal) = x";
 by Auto_tac;  
 qed "hypreal_sum_of_halves";
 
-Goal "Numeral0 < r ==> Numeral0 < r/(# 2::hypreal)";
+Goal "Numeral0 < r ==> Numeral0 < r/(2::hypreal)";
 by Auto_tac;  
 qed "hypreal_half_gt_zero";
 
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/Hyperreal/Series.ML
--- a/src/HOL/Hyperreal/Series.ML	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Hyperreal/Series.ML	Sat Oct 06 00:02:46 2001 +0200
@@ -101,7 +101,7 @@
 by (Auto_tac);
 qed "sumr_shift_bounds";
 
-Goal "sumr 0 (# 2*n) (%i. (# -1) ^ Suc i) = Numeral0";
+Goal "sumr 0 (2*n) (%i. (-1) ^ Suc i) = Numeral0";
 by (induct_tac "n" 1);
 by (Auto_tac);
 qed "sumr_minus_one_realpow_zero";
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/Hyperreal/hypreal_arith0.ML
--- a/src/HOL/Hyperreal/hypreal_arith0.ML	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Hyperreal/hypreal_arith0.ML	Sat Oct 06 00:02:46 2001 +0200
@@ -115,7 +115,7 @@
 qed "";
 
 Goal "!!a::hypreal. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
-\     ==> # 6*a <= # 5*l+i";
+\     ==> 6*a <= 5*l+i";
 by (fast_arith_tac 1);
 qed "";
 *)
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/IMP/Compiler.thy
--- a/src/HOL/IMP/Compiler.thy	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/IMP/Compiler.thy	Sat Oct 06 00:02:46 2001 +0200
@@ -39,9 +39,9 @@
 "compile (x:==a) = [ASIN x a]"
 "compile (c1;c2) = compile c1 @ compile c2"
 "compile (IF b THEN c1 ELSE c2) =
- [JMPF b (length(compile c1) + # 2)] @ compile c1 @
+ [JMPF b (length(compile c1) + 2)] @ compile c1 @
  [JMPF (%x. False) (length(compile c2)+1)] @ compile c2"
-"compile (WHILE b DO c) = [JMPF b (length(compile c) + # 2)] @ compile c @
+"compile (WHILE b DO c) = [JMPF b (length(compile c) + 2)] @ compile c @
  [JMPB (length(compile c)+1)]"
 
 declare nth_append[simp];
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/IMP/Examples.ML
--- a/src/HOL/IMP/Examples.ML	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/IMP/Examples.ML	Sat Oct 06 00:02:46 2001 +0200
@@ -34,7 +34,7 @@
 val step = resolve_tac evalc.intrs 1;
 val simp = Asm_simp_tac 1;
 Goalw [factorial_def] "a~=b ==> \
-\ <factorial a b, Mem(a:=# 3)>  -c-> Mem(b:=# 6,a:=Numeral0)";
+\ <factorial a b, Mem(a:=3)>  -c-> Mem(b:=6,a:=Numeral0)";
 by (ftac not_sym 1);
 by step;
 by  step;
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/IMPP/EvenOdd.ML
--- a/src/HOL/IMPP/EvenOdd.ML	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/IMPP/EvenOdd.ML	Sat Oct 06 00:02:46 2001 +0200
@@ -17,7 +17,7 @@
 Addsimps [not_even_1];
 
 Goalw [even_def] "even (Suc (Suc n)) = even n";
-by (subgoal_tac "Suc (Suc n) = n+# 2" 1);
+by (subgoal_tac "Suc (Suc n) = n+2" 1);
 by  (Simp_tac 2);
 by (etac ssubst 1);
 by (rtac dvd_reduce 1);
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/IMPP/EvenOdd.thy
--- a/src/HOL/IMPP/EvenOdd.thy	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/IMPP/EvenOdd.thy	Sat Oct 06 00:02:46 2001 +0200
@@ -9,7 +9,7 @@
 EvenOdd = Misc +
 
 constdefs even :: nat => bool
-  "even n == # 2 dvd n"
+  "even n == 2 dvd n"
 
 consts
   Even, Odd :: pname
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/Induct/Mutil.thy
--- a/src/HOL/Induct/Mutil.thy	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Induct/Mutil.thy	Sat Oct 06 00:02:46 2001 +0200
@@ -29,7 +29,7 @@
 
 constdefs
   coloured :: "nat => (nat \<times> nat) set"
-   "coloured b == {(i, j). (i + j) mod # 2 = b}"
+   "coloured b == {(i, j). (i + j) mod 2 = b}"
 
 
 text {* \medskip The union of two disjoint tilings is a tiling *}
@@ -61,14 +61,14 @@
   apply auto
   done
 
-lemma dominoes_tile_row [intro!]: "{i} \<times> lessThan (# 2 * n) \<in> tiling domino"
+lemma dominoes_tile_row [intro!]: "{i} \<times> lessThan (2 * n) \<in> tiling domino"
   apply (induct n)
    apply (simp_all add: Un_assoc [symmetric])
   apply (rule tiling.Un)
     apply (auto simp add: sing_Times_lemma)
   done
 
-lemma dominoes_tile_matrix: "(lessThan m) \<times> lessThan (# 2 * n) \<in> tiling domino"
+lemma dominoes_tile_matrix: "(lessThan m) \<times> lessThan (2 * n) \<in> tiling domino"
   apply (induct m)
    apply auto
   done
@@ -78,7 +78,7 @@
 
 lemma coloured_insert [simp]:
   "coloured b \<inter> (insert (i, j) t) =
-   (if (i + j) mod # 2 = b then insert (i, j) (coloured b \<inter> t)
+   (if (i + j) mod 2 = b then insert (i, j) (coloured b \<inter> t)
     else coloured b \<inter> t)"
   apply (unfold coloured_def)
   apply auto
@@ -125,7 +125,7 @@
 
 theorem gen_mutil_not_tiling:
   "t \<in> tiling domino ==>
-    (i + j) mod # 2 = 0 ==> (m + n) mod # 2 = 0 ==>
+    (i + j) mod 2 = 0 ==> (m + n) mod 2 = 0 ==>
     {(i, j), (m, n)} \<subseteq> t
   ==> (t - {(i, j)} - {(m, n)}) \<notin> tiling domino"
   apply (rule notI)
@@ -140,8 +140,8 @@
 text {* Apply the general theorem to the well-known case *}
 
 theorem mutil_not_tiling:
-  "t = lessThan (# 2 * Suc m) \<times> lessThan (# 2 * Suc n)
-    ==> t - {(0, 0)} - {(Suc (# 2 * m), Suc (# 2 * n))} \<notin> tiling domino"
+  "t = lessThan (2 * Suc m) \<times> lessThan (2 * Suc n)
+    ==> t - {(0, 0)} - {(Suc (2 * m), Suc (2 * n))} \<notin> tiling domino"
   apply (rule gen_mutil_not_tiling)
      apply (blast intro!: dominoes_tile_matrix)
     apply auto
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/Integ/Bin.ML
--- a/src/HOL/Integ/Bin.ML	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Integ/Bin.ML	Sat Oct 06 00:02:46 2001 +0200
@@ -160,7 +160,7 @@
 
 (*The correctness of shifting.  But it doesn't seem to give a measurable
   speed-up.*)
-Goal "(# 2::int) * number_of w = number_of (w BIT False)";
+Goal "(2::int) * number_of w = number_of (w BIT False)";
 by (induct_tac "w" 1);
 by (ALLGOALS (asm_simp_tac
     (simpset() addsimps bin_mult_simps @ [zadd_zmult_distrib] @ zadd_ac)));
@@ -250,11 +250,11 @@
 by (Simp_tac 1);
 qed "zmult_1_right";
 
-Goal "# -1 * z = -(z::int)";
+Goal "-1 * z = -(z::int)";
 by (simp_tac (simpset() addsimps zcompare_rls@[zmult_zminus]) 1);
 qed "zmult_minus1";
 
-Goal "z * # -1 = -(z::int)";
+Goal "z * -1 = -(z::int)";
 by (simp_tac (simpset() addsimps zcompare_rls@[zmult_zminus_right]) 1);
 qed "zmult_minus1_right";
 
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/Integ/IntArith.ML
--- a/src/HOL/Integ/IntArith.ML	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Integ/IntArith.ML	Sat Oct 06 00:02:46 2001 +0200
@@ -168,7 +168,7 @@
 by Auto_tac;  
 qed "pos_zmult_eq_1_iff";
 
-Goal "(m*n = (Numeral1::int)) = ((m = Numeral1 & n = Numeral1) | (m = # -1 & n = # -1))";
+Goal "(m*n = (Numeral1::int)) = ((m = Numeral1 & n = Numeral1) | (m = -1 & n = -1))";
 by (case_tac "Numeral0<m" 1);
 by (asm_simp_tac (simpset() addsimps [pos_zmult_eq_1_iff]) 1);
 by (case_tac "m=Numeral0" 1);
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/Integ/IntDiv.ML
--- a/src/HOL/Integ/IntDiv.ML	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Integ/IntDiv.ML	Sat Oct 06 00:02:46 2001 +0200
@@ -84,8 +84,8 @@
 
 
 Goal "adjust a b (q,r) = (let diff = r-b in \
-\                         if Numeral0 <= diff then (# 2*q + Numeral1, diff)  \
-\                                       else (# 2*q, r))";
+\                         if Numeral0 <= diff then (2*q + Numeral1, diff)  \
+\                                       else (2*q, r))";
 by (simp_tac (simpset() addsimps [Let_def,adjust_def]) 1);
 qed "adjust_eq";
 Addsimps [adjust_eq];
@@ -103,7 +103,7 @@
 (**use with simproc to avoid re-proving the premise*)
 Goal "Numeral0 < b ==> \
 \     posDivAlg (a,b) =      \
-\      (if a<b then (Numeral0,a) else adjust a b (posDivAlg(a, # 2*b)))";
+\      (if a<b then (Numeral0,a) else adjust a b (posDivAlg(a, 2*b)))";
 by (rtac (posDivAlg_raw_eqn RS trans) 1);
 by (Asm_simp_tac 1);
 qed "posDivAlg_eqn";
@@ -141,7 +141,7 @@
 (**use with simproc to avoid re-proving the premise*)
 Goal "Numeral0 < b ==> \
 \     negDivAlg (a,b) =      \
-\      (if Numeral0<=a+b then (# -1,a+b) else adjust a b (negDivAlg(a, # 2*b)))";
+\      (if Numeral0<=a+b then (-1,a+b) else adjust a b (negDivAlg(a, 2*b)))";
 by (rtac (negDivAlg_raw_eqn RS trans) 1);
 by (Asm_simp_tac 1);
 qed "negDivAlg_eqn";
@@ -179,7 +179,7 @@
 qed "posDivAlg_0";
 Addsimps [posDivAlg_0];
 
-Goal "negDivAlg (# -1, b) = (# -1, b-Numeral1)";
+Goal "negDivAlg (-1, b) = (-1, b-Numeral1)";
 by (stac negDivAlg_raw_eqn 1);
 by Auto_tac;
 qed "negDivAlg_minus1";
@@ -272,7 +272,7 @@
 by (auto_tac (claset(), simpset() addsimps [quorem_def]));
 qed "div_neg_neg_trivial";
 
-Goal "[| (Numeral0::int) < a;  a+b <= Numeral0 |] ==> a div b = # -1";
+Goal "[| (Numeral0::int) < a;  a+b <= Numeral0 |] ==> a div b = -1";
 by (rtac quorem_div 1);
 by (auto_tac (claset(), simpset() addsimps [quorem_def]));
 qed "div_pos_neg_trivial";
@@ -290,7 +290,7 @@
 qed "mod_neg_neg_trivial";
 
 Goal "[| (Numeral0::int) < a;  a+b <= Numeral0 |] ==> a mod b = a+b";
-by (res_inst_tac [("q","# -1")] quorem_mod 1);
+by (res_inst_tac [("q","-1")] quorem_mod 1);
 by (auto_tac (claset(), simpset() addsimps [quorem_def]));
 qed "mod_pos_neg_trivial";
 
@@ -411,7 +411,7 @@
 by (simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
 qed "zdiv_zero";
 
-Goal "(Numeral0::int) < b ==> # -1 div b = # -1";
+Goal "(Numeral0::int) < b ==> -1 div b = -1";
 by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
 qed "div_eq_minus1";
 
@@ -421,11 +421,11 @@
 
 Addsimps [zdiv_zero, zmod_zero];
 
-Goal "(Numeral0::int) < b ==> # -1 div b = # -1";
+Goal "(Numeral0::int) < b ==> -1 div b = -1";
 by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
 qed "zdiv_minus1";
 
-Goal "(Numeral0::int) < b ==> # -1 mod b = b-Numeral1";
+Goal "(Numeral0::int) < b ==> -1 mod b = b-Numeral1";
 by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
 qed "zmod_minus1";
 
@@ -491,15 +491,15 @@
 qed "zdiv_1";
 Addsimps [zdiv_1];
 
-Goal "a mod (# -1::int) = Numeral0";
-by (cut_inst_tac [("a","a"),("b","# -1")] neg_mod_sign 1);
-by (cut_inst_tac [("a","a"),("b","# -1")] neg_mod_bound 2);
+Goal "a mod (-1::int) = Numeral0";
+by (cut_inst_tac [("a","a"),("b","-1")] neg_mod_sign 1);
+by (cut_inst_tac [("a","a"),("b","-1")] neg_mod_bound 2);
 by Auto_tac;
 qed "zmod_minus1_right";
 Addsimps [zmod_minus1_right];
 
-Goal "a div (# -1::int) = -a";
-by (cut_inst_tac [("a","a"),("b","# -1")] zmod_zdiv_equality 1);
+Goal "a div (-1::int) = -a";
+by (cut_inst_tac [("a","a"),("b","-1")] zmod_zdiv_equality 1);
 by Auto_tac;
 qed "zdiv_minus1_right";
 Addsimps [zdiv_minus1_right];
@@ -861,13 +861,13 @@
 
 (** computing "div" by shifting **)
 
-Goal "(Numeral0::int) <= a ==> (Numeral1 + # 2*b) div (# 2*a) = b div a";
+Goal "(Numeral0::int) <= a ==> (Numeral1 + 2*b) div (2*a) = b div a";
 by (zdiv_undefined_case_tac "a = Numeral0" 1);
 by (subgoal_tac "Numeral1 <= a" 1);
  by (arith_tac 2);
-by (subgoal_tac "Numeral1 < a * # 2" 1);
+by (subgoal_tac "Numeral1 < a * 2" 1);
  by (arith_tac 2);
-by (subgoal_tac "# 2*(Numeral1 + b mod a) <= # 2*a" 1);
+by (subgoal_tac "2*(Numeral1 + b mod a) <= 2*a" 1);
  by (rtac zmult_zle_mono2 2);
 by (auto_tac (claset(),
 	      simpset() addsimps [zadd_commute, zmult_commute, 
@@ -887,12 +887,12 @@
 qed "pos_zdiv_mult_2";
 
 
-Goal "a <= (Numeral0::int) ==> (Numeral1 + # 2*b) div (# 2*a) = (b+Numeral1) div a";
-by (subgoal_tac "(Numeral1 + # 2*(-b-Numeral1)) div (# 2 * (-a)) = (-b-Numeral1) div (-a)" 1);
+Goal "a <= (Numeral0::int) ==> (Numeral1 + 2*b) div (2*a) = (b+Numeral1) div a";
+by (subgoal_tac "(Numeral1 + 2*(-b-Numeral1)) div (2 * (-a)) = (-b-Numeral1) div (-a)" 1);
 by (rtac pos_zdiv_mult_2 2);
 by (auto_tac (claset(),
 	      simpset() addsimps [zmult_zminus_right]));
-by (subgoal_tac "(# -1 - (# 2 * b)) = - (Numeral1 + (# 2 * b))" 1);
+by (subgoal_tac "(-1 - (2 * b)) = - (Numeral1 + (2 * b))" 1);
 by (Simp_tac 2);
 by (asm_full_simp_tac (HOL_ss
 		       addsimps [zdiv_zminus_zminus, zdiff_def,
@@ -921,13 +921,13 @@
 
 (** computing "mod" by shifting (proofs resemble those for "div") **)
 
-Goal "(Numeral0::int) <= a ==> (Numeral1 + # 2*b) mod (# 2*a) = Numeral1 + # 2 * (b mod a)";
+Goal "(Numeral0::int) <= a ==> (Numeral1 + 2*b) mod (2*a) = Numeral1 + 2 * (b mod a)";
 by (zdiv_undefined_case_tac "a = Numeral0" 1);
 by (subgoal_tac "Numeral1 <= a" 1);
  by (arith_tac 2);
-by (subgoal_tac "Numeral1 < a * # 2" 1);
+by (subgoal_tac "Numeral1 < a * 2" 1);
  by (arith_tac 2);
-by (subgoal_tac "# 2*(Numeral1 + b mod a) <= # 2*a" 1);
+by (subgoal_tac "2*(Numeral1 + b mod a) <= 2*a" 1);
  by (rtac zmult_zle_mono2 2);
 by (auto_tac (claset(),
 	      simpset() addsimps [zadd_commute, zmult_commute, 
@@ -947,13 +947,13 @@
 qed "pos_zmod_mult_2";
 
 
-Goal "a <= (Numeral0::int) ==> (Numeral1 + # 2*b) mod (# 2*a) = # 2 * ((b+Numeral1) mod a) - Numeral1";
+Goal "a <= (Numeral0::int) ==> (Numeral1 + 2*b) mod (2*a) = 2 * ((b+Numeral1) mod a) - Numeral1";
 by (subgoal_tac 
-    "(Numeral1 + # 2*(-b-Numeral1)) mod (# 2*(-a)) = Numeral1 + # 2*((-b-Numeral1) mod (-a))" 1);
+    "(Numeral1 + 2*(-b-Numeral1)) mod (2*(-a)) = Numeral1 + 2*((-b-Numeral1) mod (-a))" 1);
 by (rtac pos_zmod_mult_2 2);
 by (auto_tac (claset(),
 	      simpset() addsimps [zmult_zminus_right]));
-by (subgoal_tac "(# -1 - (# 2 * b)) = - (Numeral1 + (# 2 * b))" 1);
+by (subgoal_tac "(-1 - (2 * b)) = - (Numeral1 + (2 * b))" 1);
 by (Simp_tac 2);
 by (asm_full_simp_tac (HOL_ss
 		       addsimps [zmod_zminus_zminus, zdiff_def,
@@ -965,9 +965,9 @@
 Goal "number_of (v BIT b) mod number_of (w BIT False) = \
 \         (if b then \
 \               if (Numeral0::int) <= number_of w \
-\               then # 2 * (number_of v mod number_of w) + Numeral1    \
-\               else # 2 * ((number_of v + (Numeral1::int)) mod number_of w) - Numeral1  \
-\          else # 2 * (number_of v mod number_of w))";
+\               then 2 * (number_of v mod number_of w) + Numeral1    \
+\               else 2 * ((number_of v + (Numeral1::int)) mod number_of w) - Numeral1  \
+\          else 2 * (number_of v mod number_of w))";
 by (simp_tac (simpset_of Int.thy addsimps [zadd_assoc, number_of_BIT]) 1);
 by (asm_simp_tac (simpset()
 		  delsimps bin_arith_extra_simps@bin_rel_simps
@@ -981,10 +981,10 @@
 (** Quotients of signs **)
 
 Goal "[| a < (Numeral0::int);  Numeral0 < b |] ==> a div b < Numeral0";
-by (subgoal_tac "a div b <= # -1" 1);
+by (subgoal_tac "a div b <= -1" 1);
 by (Force_tac 1);
 by (rtac order_trans 1);
-by (res_inst_tac [("a'","# -1")]  zdiv_mono1 1);
+by (res_inst_tac [("a'","-1")]  zdiv_mono1 1);
 by (auto_tac (claset(), simpset() addsimps [zdiv_minus1]));
 qed "div_neg_pos_less0";
 
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/Integ/IntDiv.thy
--- a/src/HOL/Integ/IntDiv.thy	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Integ/IntDiv.thy	Sat Oct 06 00:02:46 2001 +0200
@@ -15,8 +15,8 @@
                       (if Numeral0 < b then Numeral0<=r & r<b else b<r & r <= Numeral0)"
 
   adjust :: "[int, int, int*int] => int*int"
-    "adjust a b == %(q,r). if Numeral0 <= r-b then (# 2*q + Numeral1, r-b)
-                           else (# 2*q, r)"
+    "adjust a b == %(q,r). if Numeral0 <= r-b then (2*q + Numeral1, r-b)
+                           else (2*q, r)"
 
 (** the division algorithm **)
 
@@ -25,14 +25,14 @@
 recdef posDivAlg "inv_image less_than (%(a,b). nat(a - b + Numeral1))"
     "posDivAlg (a,b) =
        (if (a<b | b<=Numeral0) then (Numeral0,a)
-        else adjust a b (posDivAlg(a, # 2*b)))"
+        else adjust a b (posDivAlg(a, 2*b)))"
 
 (*for the case a<0, b>0*)
 consts negDivAlg :: "int*int => int*int"
 recdef negDivAlg "inv_image less_than (%(a,b). nat(- a - b))"
     "negDivAlg (a,b) =
-       (if (Numeral0<=a+b | b<=Numeral0) then (# -1,a+b)
-        else adjust a b (negDivAlg(a, # 2*b)))"
+       (if (Numeral0<=a+b | b<=Numeral0) then (-1,a+b)
+        else adjust a b (negDivAlg(a, 2*b)))"
 
 (*for the general case b~=0*)
 
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/Integ/NatSimprocs.ML
--- a/src/HOL/Integ/NatSimprocs.ML	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Integ/NatSimprocs.ML	Sat Oct 06 00:02:46 2001 +0200
@@ -92,40 +92,40 @@
 
 (** Evens and Odds, for Mutilated Chess Board **)
 
-(*Case analysis on b<# 2*)
-Goal "(n::nat) < # 2 ==> n = Numeral0 | n = Numeral1";
+(*Case analysis on b<2*)
+Goal "(n::nat) < 2 ==> n = Numeral0 | n = Numeral1";
 by (arith_tac 1);
 qed "less_2_cases";
 
-Goal "Suc(Suc(m)) mod # 2 = m mod # 2";
-by (subgoal_tac "m mod # 2 < # 2" 1);
+Goal "Suc(Suc(m)) mod 2 = m mod 2";
+by (subgoal_tac "m mod 2 < 2" 1);
 by (Asm_simp_tac 2);
 be (less_2_cases RS disjE) 1;
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_Suc])));
 qed "mod2_Suc_Suc";
 Addsimps [mod2_Suc_Suc];
 
-Goal "!!m::nat. (0 < m mod # 2) = (m mod # 2 = Numeral1)";
-by (subgoal_tac "m mod # 2 < # 2" 1);
+Goal "!!m::nat. (0 < m mod 2) = (m mod 2 = Numeral1)";
+by (subgoal_tac "m mod 2 < 2" 1);
 by (Asm_simp_tac 2);
 by (auto_tac (claset(), simpset() delsimps [mod_less_divisor]));
 qed "mod2_gr_0";
 Addsimps [mod2_gr_0, rename_numerals mod2_gr_0];
 
-(** Removal of small numerals: Numeral0, Numeral1 and (in additive positions) # 2 **)
+(** Removal of small numerals: Numeral0, Numeral1 and (in additive positions) 2 **)
 
-Goal "# 2 + n = Suc (Suc n)";
+Goal "2 + n = Suc (Suc n)";
 by (Simp_tac 1);
 qed "add_2_eq_Suc";
 
-Goal "n + # 2 = Suc (Suc n)";
+Goal "n + 2 = Suc (Suc n)";
 by (Simp_tac 1);
 qed "add_2_eq_Suc'";
 
 Addsimps [numeral_0_eq_0, numeral_1_eq_1, add_2_eq_Suc, add_2_eq_Suc'];
 
 (*Can be used to eliminate long strings of Sucs, but not by default*)
-Goal "Suc (Suc (Suc n)) = # 3 + n";
+Goal "Suc (Suc (Suc n)) = 3 + n";
 by (Simp_tac 1);
 qed "Suc3_eq_add_3";
 
@@ -136,21 +136,21 @@
     We already have some rules to simplify operands smaller than 3.
 **)
 
-Goal "m div (Suc (Suc (Suc n))) = m div (# 3+n)";
+Goal "m div (Suc (Suc (Suc n))) = m div (3+n)";
 by (simp_tac (simpset() addsimps [Suc3_eq_add_3]) 1);
 qed "div_Suc_eq_div_add3";
 
-Goal "m mod (Suc (Suc (Suc n))) = m mod (# 3+n)";
+Goal "m mod (Suc (Suc (Suc n))) = m mod (3+n)";
 by (simp_tac (simpset() addsimps [Suc3_eq_add_3]) 1);
 qed "mod_Suc_eq_mod_add3";
 
 Addsimps [div_Suc_eq_div_add3, mod_Suc_eq_mod_add3];
 
-Goal "(Suc (Suc (Suc m))) div n = (# 3+m) div n";
+Goal "(Suc (Suc (Suc m))) div n = (3+m) div n";
 by (simp_tac (simpset() addsimps [Suc3_eq_add_3]) 1);
 qed "Suc_div_eq_add3_div";
 
-Goal "(Suc (Suc (Suc m))) mod n = (# 3+m) mod n";
+Goal "(Suc (Suc (Suc m))) mod n = (3+m) mod n";
 by (simp_tac (simpset() addsimps [Suc3_eq_add_3]) 1);
 qed "Suc_mod_eq_add3_mod";
 
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/Integ/int_arith1.ML
--- a/src/HOL/Integ/int_arith1.ML	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Integ/int_arith1.ML	Sat Oct 06 00:02:46 2001 +0200
@@ -279,7 +279,7 @@
 structure CombineNumeralsData =
   struct
   val add		= op + : int*int -> int 
-  val mk_sum    	= long_mk_sum    (*to work for e.g. # 2*x + # 3*x *)
+  val mk_sum    	= long_mk_sum    (*to work for e.g. 2*x + 3*x *)
   val dest_sum		= dest_sum
   val mk_coeff		= mk_coeff
   val dest_coeff	= dest_coeff 1
@@ -318,35 +318,35 @@
 set trace_simp;
 fun test s = (Goal s; by (Simp_tac 1)); 
 
-test "l + # 2 + # 2 + # 2 + (l + # 2) + (oo + # 2) = (uu::int)";
+test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)";
 
-test "# 2*u = (u::int)";
-test "(i + j + # 12 + (k::int)) - # 15 = y";
-test "(i + j + # 12 + (k::int)) - # 5 = y";
+test "2*u = (u::int)";
+test "(i + j + 12 + (k::int)) - 15 = y";
+test "(i + j + 12 + (k::int)) - 5 = y";
 
 test "y - b < (b::int)";
-test "y - (# 3*b + c) < (b::int) - # 2*c";
+test "y - (3*b + c) < (b::int) - 2*c";
 
-test "(# 2*x - (u*v) + y) - v*# 3*u = (w::int)";
-test "(# 2*x*u*v + (u*v)*# 4 + y) - v*u*# 4 = (w::int)";
-test "(# 2*x*u*v + (u*v)*# 4 + y) - v*u = (w::int)";
-test "u*v - (x*u*v + (u*v)*# 4 + y) = (w::int)";
+test "(2*x - (u*v) + y) - v*3*u = (w::int)";
+test "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::int)";
+test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::int)";
+test "u*v - (x*u*v + (u*v)*4 + y) = (w::int)";
 
-test "(i + j + # 12 + (k::int)) = u + # 15 + y";
-test "(i + j*# 2 + # 12 + (k::int)) = j + # 5 + y";
+test "(i + j + 12 + (k::int)) = u + 15 + y";
+test "(i + j*2 + 12 + (k::int)) = j + 5 + y";
 
-test "# 2*y + # 3*z + # 6*w + # 2*y + # 3*z + # 2*u = # 2*y' + # 3*z' + # 6*w' + # 2*y' + # 3*z' + u + (vv::int)";
+test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + (vv::int)";
 
 test "a + -(b+c) + b = (d::int)";
 test "a + -(b+c) - b = (d::int)";
 
 (*negative numerals*)
-test "(i + j + # -2 + (k::int)) - (u + # 5 + y) = zz";
-test "(i + j + # -3 + (k::int)) < u + # 5 + y";
-test "(i + j + # 3 + (k::int)) < u + # -6 + y";
-test "(i + j + # -12 + (k::int)) - # 15 = y";
-test "(i + j + # 12 + (k::int)) - # -15 = y";
-test "(i + j + # -12 + (k::int)) - # -15 = y";
+test "(i + j + -2 + (k::int)) - (u + 5 + y) = zz";
+test "(i + j + -3 + (k::int)) < u + 5 + y";
+test "(i + j + 3 + (k::int)) < u + -6 + y";
+test "(i + j + -12 + (k::int)) - 15 = y";
+test "(i + j + 12 + (k::int)) - -15 = y";
+test "(i + j + -12 + (k::int)) - -15 = y";
 *)
 
 
@@ -455,7 +455,7 @@
 (* Some test data
 Goal "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
 by (fast_arith_tac 1);
-Goal "!!a::int. [| a < b; c < d |] ==> a-d+ # 2 <= b+(-c)";
+Goal "!!a::int. [| a < b; c < d |] ==> a-d+ 2 <= b+(-c)";
 by (fast_arith_tac 1);
 Goal "!!a::int. [| a < b; c < d |] ==> a+c+ Numeral1 < b+d";
 by (fast_arith_tac 1);
@@ -465,7 +465,7 @@
 \     ==> a+a <= j+j";
 by (fast_arith_tac 1);
 Goal "!!a::int. [| a+b < i+j; a<b; i<j |] \
-\     ==> a+a - - # -1 < j+j - # 3";
+\     ==> a+a - - -1 < j+j - 3";
 by (fast_arith_tac 1);
 Goal "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
 by (arith_tac 1);
@@ -482,6 +482,6 @@
 \     ==> a+a+a+a+a+a <= l+l+l+l+i+l";
 by (fast_arith_tac 1);
 Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
-\     ==> # 6*a <= # 5*l+i";
+\     ==> 6*a <= 5*l+i";
 by (fast_arith_tac 1);
 *)
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/Integ/int_arith2.ML
--- a/src/HOL/Integ/int_arith2.ML	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Integ/int_arith2.ML	Sat Oct 06 00:02:46 2001 +0200
@@ -75,7 +75,7 @@
 by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
 qed "nat_1";
 
-Goal "nat # 2 = Suc (Suc 0)";
+Goal "nat 2 = Suc (Suc 0)";
 by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
 qed "nat_2";
 
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/Integ/int_factor_simprocs.ML
--- a/src/HOL/Integ/int_factor_simprocs.ML	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Integ/int_factor_simprocs.ML	Sat Oct 06 00:02:46 2001 +0200
@@ -114,33 +114,33 @@
 set trace_simp;
 fun test s = (Goal s; by (Simp_tac 1)); 
 
-test "# 9*x = # 12 * (y::int)";
-test "(# 9*x) div (# 12 * (y::int)) = z";
-test "# 9*x < # 12 * (y::int)";
-test "# 9*x <= # 12 * (y::int)";
+test "9*x = 12 * (y::int)";
+test "(9*x) div (12 * (y::int)) = z";
+test "9*x < 12 * (y::int)";
+test "9*x <= 12 * (y::int)";
 
-test "# -99*x = # 132 * (y::int)";
-test "(# -99*x) div (# 132 * (y::int)) = z";
-test "# -99*x < # 132 * (y::int)";
-test "# -99*x <= # 132 * (y::int)";
+test "-99*x = 132 * (y::int)";
+test "(-99*x) div (132 * (y::int)) = z";
+test "-99*x < 132 * (y::int)";
+test "-99*x <= 132 * (y::int)";
 
-test "# 999*x = # -396 * (y::int)";
-test "(# 999*x) div (# -396 * (y::int)) = z";
-test "# 999*x < # -396 * (y::int)";
-test "# 999*x <= # -396 * (y::int)";
+test "999*x = -396 * (y::int)";
+test "(999*x) div (-396 * (y::int)) = z";
+test "999*x < -396 * (y::int)";
+test "999*x <= -396 * (y::int)";
 
-test "# -99*x = # -81 * (y::int)";
-test "(# -99*x) div (# -81 * (y::int)) = z";
-test "# -99*x <= # -81 * (y::int)";
-test "# -99*x < # -81 * (y::int)";
+test "-99*x = -81 * (y::int)";
+test "(-99*x) div (-81 * (y::int)) = z";
+test "-99*x <= -81 * (y::int)";
+test "-99*x < -81 * (y::int)";
 
-test "# -2 * x = # -1 * (y::int)";
-test "# -2 * x = -(y::int)";
-test "(# -2 * x) div (# -1 * (y::int)) = z";
-test "# -2 * x < -(y::int)";
-test "# -2 * x <= # -1 * (y::int)";
-test "-x < # -23 * (y::int)";
-test "-x <= # -23 * (y::int)";
+test "-2 * x = -1 * (y::int)";
+test "-2 * x = -(y::int)";
+test "(-2 * x) div (-1 * (y::int)) = z";
+test "-2 * x < -(y::int)";
+test "-2 * x <= -1 * (y::int)";
+test "-x < -23 * (y::int)";
+test "-x <= -23 * (y::int)";
 *)
 
 
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/Integ/nat_bin.ML
--- a/src/HOL/Integ/nat_bin.ML	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Integ/nat_bin.ML	Sat Oct 06 00:02:46 2001 +0200
@@ -25,7 +25,7 @@
 by (simp_tac (HOL_basic_ss addsimps [nat_1, nat_number_of_def, One_nat_def]) 1);
 qed "numeral_1_eq_1";
 
-Goal "# 2 = Suc 1";
+Goal "2 = Suc 1";
 by (simp_tac (HOL_basic_ss addsimps [nat_2, nat_number_of_def, One_nat_def]) 1);
 qed "numeral_2_eq_2";
 
@@ -77,7 +77,7 @@
 by (Simp_tac 1);
 qed "Suc_numeral_0_eq_1";
 
-Goal "Suc Numeral1 = # 2";
+Goal "Suc Numeral1 = 2";
 by (Simp_tac 1);
 qed "Suc_numeral_1_eq_2";
 
@@ -384,7 +384,7 @@
 qed "power_one";
 Addsimps [power_zero, power_one];
 
-Goal "(p::nat) ^ # 2 = p*p";
+Goal "(p::nat) ^ 2 = p*p";
 by (simp_tac numeral_ss 1);
 qed "power_two";
 
@@ -497,7 +497,7 @@
 
 Goal "m+m ~= int (Suc 0) + n + n";
 by Auto_tac;
-by (dres_inst_tac [("f", "%x. x mod # 2")] arg_cong 1);
+by (dres_inst_tac [("f", "%x. x mod 2")] arg_cong 1);
 by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); 
 val lemma2 = result();
 
@@ -514,7 +514,7 @@
 by (res_inst_tac [("x", "number_of v")] spec 1);
 by Safe_tac;
 by (ALLGOALS Full_simp_tac);
-by (dres_inst_tac [("f", "%x. x mod # 2")] arg_cong 1);
+by (dres_inst_tac [("f", "%x. x mod 2")] arg_cong 1);
 by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); 
 qed "eq_number_of_BIT_Pls"; 
 
@@ -524,7 +524,7 @@
 	       [number_of_BIT, number_of_Min, eq_commute]) 1); 
 by (res_inst_tac [("x", "number_of v")] spec 1);
 by Auto_tac;
-by (dres_inst_tac [("f", "%x. x mod # 2")] arg_cong 1);
+by (dres_inst_tac [("f", "%x. x mod 2")] arg_cong 1);
 by Auto_tac;
 qed "eq_number_of_BIT_Min"; 
 
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/Integ/nat_simprocs.ML
--- a/src/HOL/Integ/nat_simprocs.ML	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Integ/nat_simprocs.ML	Sat Oct 06 00:02:46 2001 +0200
@@ -319,7 +319,7 @@
 structure CombineNumeralsData =
   struct
   val add		= op + : int*int -> int 
-  val mk_sum            = long_mk_sum    (*to work for e.g. # 2*x + # 3*x *)
+  val mk_sum            = long_mk_sum    (*to work for e.g. 2*x + 3*x *)
   val dest_sum          = restricted_dest_Sucs_sum
   val mk_coeff          = mk_coeff
   val dest_coeff        = dest_coeff
@@ -504,62 +504,62 @@
 fun test s = (Goal s; by (Simp_tac 1));
 
 (*cancel_numerals*)
-test "l +( # 2) + (# 2) + # 2 + (l + # 2) + (oo  + # 2) = (uu::nat)";
-test "(# 2*length xs < # 2*length xs + j)";
-test "(# 2*length xs < length xs * # 2 + j)";
-test "# 2*u = (u::nat)";
-test "# 2*u = Suc (u)";
-test "(i + j + # 12 + (k::nat)) - # 15 = y";
-test "(i + j + # 12 + (k::nat)) - # 5 = y";
-test "Suc u - # 2 = y";
-test "Suc (Suc (Suc u)) - # 2 = y";
-test "(i + j + # 2 + (k::nat)) - 1 = y";
+test "l +( 2) + (2) + 2 + (l + 2) + (oo  + 2) = (uu::nat)";
+test "(2*length xs < 2*length xs + j)";
+test "(2*length xs < length xs * 2 + j)";
+test "2*u = (u::nat)";
+test "2*u = Suc (u)";
+test "(i + j + 12 + (k::nat)) - 15 = y";
+test "(i + j + 12 + (k::nat)) - 5 = y";
+test "Suc u - 2 = y";
+test "Suc (Suc (Suc u)) - 2 = y";
+test "(i + j + 2 + (k::nat)) - 1 = y";
 test "(i + j + Numeral1 + (k::nat)) - 2 = y";
 
-test "(# 2*x + (u*v) + y) - v*# 3*u = (w::nat)";
-test "(# 2*x*u*v + # 5 + (u*v)*# 4 + y) - v*u*# 4 = (w::nat)";
-test "(# 2*x*u*v + (u*v)*# 4 + y) - v*u = (w::nat)";
-test "Suc (Suc (# 2*x*u*v + u*# 4 + y)) - u = w";
-test "Suc ((u*v)*# 4) - v*# 3*u = w";
-test "Suc (Suc ((u*v)*# 3)) - v*# 3*u = w";
+test "(2*x + (u*v) + y) - v*3*u = (w::nat)";
+test "(2*x*u*v + 5 + (u*v)*4 + y) - v*u*4 = (w::nat)";
+test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::nat)";
+test "Suc (Suc (2*x*u*v + u*4 + y)) - u = w";
+test "Suc ((u*v)*4) - v*3*u = w";
+test "Suc (Suc ((u*v)*3)) - v*3*u = w";
 
-test "(i + j + # 12 + (k::nat)) = u + # 15 + y";
-test "(i + j + # 32 + (k::nat)) - (u + # 15 + y) = zz";
-test "(i + j + # 12 + (k::nat)) = u + # 5 + y";
+test "(i + j + 12 + (k::nat)) = u + 15 + y";
+test "(i + j + 32 + (k::nat)) - (u + 15 + y) = zz";
+test "(i + j + 12 + (k::nat)) = u + 5 + y";
 (*Suc*)
-test "(i + j + # 12 + k) = Suc (u + y)";
-test "Suc (Suc (Suc (Suc (Suc (u + y))))) <= ((i + j) + # 41 + k)";
-test "(i + j + # 5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))";
-test "Suc (Suc (Suc (Suc (Suc (u + y))))) - # 5 = v";
-test "(i + j + # 5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))";
-test "# 2*y + # 3*z + # 2*u = Suc (u)";
-test "# 2*y + # 3*z + # 6*w + # 2*y + # 3*z + # 2*u = Suc (u)";
-test "# 2*y + # 3*z + # 6*w + # 2*y + # 3*z + # 2*u = # 2*y' + # 3*z' + # 6*w' + # 2*y' + # 3*z' + u + (vv::nat)";
-test "# 6 + # 2*y + # 3*z + # 4*u = Suc (vv + # 2*u + z)";
-test "(# 2*n*m) < (# 3*(m*n)) + (u::nat)";
+test "(i + j + 12 + k) = Suc (u + y)";
+test "Suc (Suc (Suc (Suc (Suc (u + y))))) <= ((i + j) + 41 + k)";
+test "(i + j + 5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))";
+test "Suc (Suc (Suc (Suc (Suc (u + y))))) - 5 = v";
+test "(i + j + 5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))";
+test "2*y + 3*z + 2*u = Suc (u)";
+test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = Suc (u)";
+test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + (vv::nat)";
+test "6 + 2*y + 3*z + 4*u = Suc (vv + 2*u + z)";
+test "(2*n*m) < (3*(m*n)) + (u::nat)";
 
 (*negative numerals: FAIL*)
-test "(i + j + # -23 + (k::nat)) < u + # 15 + y";
-test "(i + j + # 3 + (k::nat)) < u + # -15 + y";
-test "(i + j + # -12 + (k::nat)) - # 15 = y";
-test "(i + j + # 12 + (k::nat)) - # -15 = y";
-test "(i + j + # -12 + (k::nat)) - # -15 = y";
+test "(i + j + -23 + (k::nat)) < u + 15 + y";
+test "(i + j + 3 + (k::nat)) < u + -15 + y";
+test "(i + j + -12 + (k::nat)) - 15 = y";
+test "(i + j + 12 + (k::nat)) - -15 = y";
+test "(i + j + -12 + (k::nat)) - -15 = y";
 
 (*combine_numerals*)
-test "k + # 3*k = (u::nat)";
-test "Suc (i + # 3) = u";
-test "Suc (i + j + # 3 + k) = u";
-test "k + j + # 3*k + j = (u::nat)";
-test "Suc (j*i + i + k + # 5 + # 3*k + i*j*# 4) = (u::nat)";
-test "(# 2*n*m) + (# 3*(m*n)) = (u::nat)";
+test "k + 3*k = (u::nat)";
+test "Suc (i + 3) = u";
+test "Suc (i + j + 3 + k) = u";
+test "k + j + 3*k + j = (u::nat)";
+test "Suc (j*i + i + k + 5 + 3*k + i*j*4) = (u::nat)";
+test "(2*n*m) + (3*(m*n)) = (u::nat)";
 (*negative numerals: FAIL*)
-test "Suc (i + j + # -3 + k) = u";
+test "Suc (i + j + -3 + k) = u";
 
 (*cancel_numeral_factors*)
-test "# 9*x = # 12 * (y::nat)";
-test "(# 9*x) div (# 12 * (y::nat)) = z";
-test "# 9*x < # 12 * (y::nat)";
-test "# 9*x <= # 12 * (y::nat)";
+test "9*x = 12 * (y::nat)";
+test "(9*x) div (12 * (y::nat)) = z";
+test "9*x < 12 * (y::nat)";
+test "9*x <= 12 * (y::nat)";
 
 (*cancel_factor*)
 test "x*k = k*(y::nat)";
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/Isar_examples/Fibonacci.thy
--- a/src/HOL/Isar_examples/Fibonacci.thy	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Isar_examples/Fibonacci.thy	Sat Oct 06 00:02:46 2001 +0200
@@ -39,7 +39,7 @@
 text {* Alternative induction rule. *}
 
 theorem fib_induct:
-    "P 0 ==> P 1 ==> (!!n. P (n + 1) ==> P n ==> P (n + # 2)) ==> P (n::nat)"
+    "P 0 ==> P 1 ==> (!!n. P (n + 1) ==> P n ==> P (n + 2)) ==> P (n::nat)"
   by (induct rule: fib.induct, simp+)
 
 
@@ -56,7 +56,7 @@
   show "?P 0" by simp
   show "?P 1" by simp
   fix n
-  have "fib (n + # 2 + k + 1)
+  have "fib (n + 2 + k + 1)
     = fib (n + k + 1) + fib (n + 1 + k + 1)" by simp
   also assume "fib (n + k + 1)
     = fib (k + 1) * fib (n + 1) + fib k * fib n"
@@ -65,9 +65,9 @@
     = fib (k + 1) * fib (n + 1 + 1) + fib k * fib (n + 1)"
       (is " _ = ?R2")
   also have "?R1 + ?R2
-    = fib (k + 1) * fib (n + # 2 + 1) + fib k * fib (n + # 2)"
+    = fib (k + 1) * fib (n + 2 + 1) + fib k * fib (n + 2)"
     by (simp add: add_mult_distrib2)
-  finally show "?P (n + # 2)" .
+  finally show "?P (n + 2)" .
 qed
 
 lemma gcd_fib_Suc_eq_1: "gcd (fib n, fib (n + 1)) = 1" (is "?P n")
@@ -75,14 +75,14 @@
   show "?P 0" by simp
   show "?P 1" by simp
   fix n
-  have "fib (n + # 2 + 1) = fib (n + 1) + fib (n + # 2)"
+  have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)"
     by simp
-  also have "gcd (fib (n + # 2), ...) = gcd (fib (n + # 2), fib (n + 1))"
+  also have "gcd (fib (n + 2), ...) = gcd (fib (n + 2), fib (n + 1))"
     by (simp only: gcd_add2')
   also have "... = gcd (fib (n + 1), fib (n + 1 + 1))"
     by (simp add: gcd_commute)
   also assume "... = 1"
-  finally show "?P (n + # 2)" .
+  finally show "?P (n + 2)" .
 qed
 
 lemma gcd_mult_add: "0 < n ==> gcd (n * k + m, n) = gcd (m, n)"
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/Isar_examples/HoareEx.thy
--- a/src/HOL/Isar_examples/HoareEx.thy	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Isar_examples/HoareEx.thy	Sat Oct 06 00:02:46 2001 +0200
@@ -39,7 +39,7 @@
 *}
 
 lemma
-  "|- .{\<acute>(N_update (# 2 * \<acute>N)) : .{\<acute>N = # 10}.}. \<acute>N := # 2 * \<acute>N .{\<acute>N = # 10}."
+  "|- .{\<acute>(N_update (2 * \<acute>N)) : .{\<acute>N = 10}.}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}."
   by (rule assign)
 
 text {*
@@ -49,13 +49,13 @@
  ``obvious'' consequences as well.
 *}
 
-lemma "|- .{True}. \<acute>N := # 10 .{\<acute>N = # 10}."
+lemma "|- .{True}. \<acute>N := 10 .{\<acute>N = 10}."
   by hoare
 
-lemma "|- .{# 2 * \<acute>N = # 10}. \<acute>N := # 2 * \<acute>N .{\<acute>N = # 10}."
+lemma "|- .{2 * \<acute>N = 10}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}."
   by hoare
 
-lemma "|- .{\<acute>N = # 5}. \<acute>N := # 2 * \<acute>N .{\<acute>N = # 10}."
+lemma "|- .{\<acute>N = 5}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}."
   by hoare simp
 
 lemma "|- .{\<acute>N + 1 = a + 1}. \<acute>N := \<acute>N + 1 .{\<acute>N = a + 1}."
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/Isar_examples/MutilatedCheckerboard.thy
--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Sat Oct 06 00:02:46 2001 +0200
@@ -76,7 +76,7 @@
   by (simp add: below_def less_Suc_eq) blast
 
 lemma Sigma_Suc2:
-    "m = n + # 2 ==> A <*> below m =
+    "m = n + 2 ==> A <*> below m =
       (A <*> {n}) Un (A <*> {n + 1}) Un (A <*> below n)"
   by (auto simp add: below_def) arith
 
@@ -87,10 +87,10 @@
 
 constdefs
   evnodd :: "(nat * nat) set => nat => (nat * nat) set"
-  "evnodd A b == A Int {(i, j). (i + j) mod # 2 = b}"
+  "evnodd A b == A Int {(i, j). (i + j) mod 2 = b}"
 
 lemma evnodd_iff:
-    "(i, j): evnodd A b = ((i, j): A  & (i + j) mod # 2 = b)"
+    "(i, j): evnodd A b = ((i, j): A  & (i + j) mod 2 = b)"
   by (simp add: evnodd_def)
 
 lemma evnodd_subset: "evnodd A b <= A"
@@ -112,7 +112,7 @@
   by (simp add: evnodd_def)
 
 lemma evnodd_insert: "evnodd (insert (i, j) C) b =
-    (if (i + j) mod # 2 = b
+    (if (i + j) mod 2 = b
       then insert (i, j) (evnodd C b) else evnodd C b)"
   by (simp add: evnodd_def) blast
 
@@ -128,21 +128,21 @@
     vertl: "{(i, j), (i + 1, j)} : domino"
 
 lemma dominoes_tile_row:
-  "{i} <*> below (# 2 * n) : tiling domino"
+  "{i} <*> below (2 * n) : tiling domino"
   (is "?P n" is "?B n : ?T")
 proof (induct n)
   show "?P 0" by (simp add: below_0 tiling.empty)
 
   fix n assume hyp: "?P n"
-  let ?a = "{i} <*> {# 2 * n + 1} Un {i} <*> {# 2 * n}"
+  let ?a = "{i} <*> {2 * n + 1} Un {i} <*> {2 * n}"
 
   have "?B (Suc n) = ?a Un ?B n"
     by (auto simp add: Sigma_Suc Un_assoc)
   also have "... : ?T"
   proof (rule tiling.Un)
-    have "{(i, # 2 * n), (i, # 2 * n + 1)} : domino"
+    have "{(i, 2 * n), (i, 2 * n + 1)} : domino"
       by (rule domino.horiz)
-    also have "{(i, # 2 * n), (i, # 2 * n + 1)} = ?a" by blast
+    also have "{(i, 2 * n), (i, 2 * n + 1)} = ?a" by blast
     finally show "... : domino" .
     from hyp show "?B n : ?T" .
     show "?a <= - ?B n" by blast
@@ -151,13 +151,13 @@
 qed
 
 lemma dominoes_tile_matrix:
-  "below m <*> below (# 2 * n) : tiling domino"
+  "below m <*> below (2 * n) : tiling domino"
   (is "?P m" is "?B m : ?T")
 proof (induct m)
   show "?P 0" by (simp add: below_0 tiling.empty)
 
   fix m assume hyp: "?P m"
-  let ?t = "{m} <*> below (# 2 * n)"
+  let ?t = "{m} <*> below (2 * n)"
 
   have "?B (Suc m) = ?t Un ?B m" by (simp add: Sigma_Suc)
   also have "... : ?T"
@@ -170,9 +170,9 @@
 qed
 
 lemma domino_singleton:
-  "d : domino ==> b < # 2 ==> EX i j. evnodd d b = {(i, j)}"
+  "d : domino ==> b < 2 ==> EX i j. evnodd d b = {(i, j)}"
 proof -
-  assume b: "b < # 2"
+  assume b: "b < 2"
   assume "d : domino"
   thus ?thesis (is "?P d")
   proof induct
@@ -227,9 +227,9 @@
       and at: "a <= - t"
 
     have card_suc:
-      "!!b. b < # 2 ==> card (?e (a Un t) b) = Suc (card (?e t b))"
+      "!!b. b < 2 ==> card (?e (a Un t) b) = Suc (card (?e t b))"
     proof -
-      fix b :: nat assume "b < # 2"
+      fix b :: nat assume "b < 2"
       have "?e (a Un t) b = ?e a b Un ?e t b" by (rule evnodd_Un)
       also obtain i j where e: "?e a b = {(i, j)}"
       proof -
@@ -260,15 +260,15 @@
 constdefs
   mutilated_board :: "nat => nat => (nat * nat) set"
   "mutilated_board m n ==
-    below (# 2 * (m + 1)) <*> below (# 2 * (n + 1))
-      - {(0, 0)} - {(# 2 * m + 1, # 2 * n + 1)}"
+    below (2 * (m + 1)) <*> below (2 * (n + 1))
+      - {(0, 0)} - {(2 * m + 1, 2 * n + 1)}"
 
 theorem mutil_not_tiling: "mutilated_board m n ~: tiling domino"
 proof (unfold mutilated_board_def)
   let ?T = "tiling domino"
-  let ?t = "below (# 2 * (m + 1)) <*> below (# 2 * (n + 1))"
+  let ?t = "below (2 * (m + 1)) <*> below (2 * (n + 1))"
   let ?t' = "?t - {(0, 0)}"
-  let ?t'' = "?t' - {(# 2 * m + 1, # 2 * n + 1)}"
+  let ?t'' = "?t' - {(2 * m + 1, 2 * n + 1)}"
 
   show "?t'' ~: ?T"
   proof
@@ -282,12 +282,12 @@
     note [simp] = evnodd_iff evnodd_empty evnodd_insert evnodd_Diff
     have "card (?e ?t'' 0) < card (?e ?t' 0)"
     proof -
-      have "card (?e ?t' 0 - {(# 2 * m + 1, # 2 * n + 1)})
+      have "card (?e ?t' 0 - {(2 * m + 1, 2 * n + 1)})
         < card (?e ?t' 0)"
       proof (rule card_Diff1_less)
         from _ fin show "finite (?e ?t' 0)"
           by (rule finite_subset) auto
-        show "(# 2 * m + 1, # 2 * n + 1) : ?e ?t' 0" by simp
+        show "(2 * m + 1, 2 * n + 1) : ?e ?t' 0" by simp
       qed
       thus ?thesis by simp
     qed
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/Isar_examples/Summation.thy
--- a/src/HOL/Isar_examples/Summation.thy	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Isar_examples/Summation.thy	Sat Oct 06 00:02:46 2001 +0200
@@ -31,14 +31,14 @@
 *}
 
 theorem sum_of_naturals:
-  "# 2 * (\<Sum>i < n + 1. i) = n * (n + 1)"
+  "2 * (\<Sum>i < n + 1. i) = n * (n + 1)"
   (is "?P n" is "?S n = _")
 proof (induct n)
   show "?P 0" by simp
 next
-  fix n have "?S (n + 1) = ?S n + # 2 * (n + 1)" by simp
+  fix n have "?S (n + 1) = ?S n + 2 * (n + 1)" by simp
   also assume "?S n = n * (n + 1)"
-  also have "... + # 2 * (n + 1) = (n + 1) * (n + # 2)" by simp
+  also have "... + 2 * (n + 1) = (n + 1) * (n + 2)" by simp
   finally show "?P (Suc n)" by simp
 qed
 
@@ -86,14 +86,14 @@
 *}
 
 theorem sum_of_odds:
-  "(\<Sum>i < n. # 2 * i + 1) = n^Suc (Suc 0)"
+  "(\<Sum>i < n. 2 * i + 1) = n^Suc (Suc 0)"
   (is "?P n" is "?S n = _")
 proof (induct n)
   show "?P 0" by simp
 next
-  fix n have "?S (n + 1) = ?S n + # 2 * n + 1" by simp
+  fix n have "?S (n + 1) = ?S n + 2 * n + 1" by simp
   also assume "?S n = n^Suc (Suc 0)"
-  also have "... + # 2 * n + 1 = (n + 1)^Suc (Suc 0)" by simp
+  also have "... + 2 * n + 1 = (n + 1)^Suc (Suc 0)" by simp
   finally show "?P (Suc n)" by simp
 qed
 
@@ -106,28 +106,28 @@
 lemmas distrib = add_mult_distrib add_mult_distrib2
 
 theorem sum_of_squares:
-  "# 6 * (\<Sum>i < n + 1. i^Suc (Suc 0)) = n * (n + 1) * (# 2 * n + 1)"
+  "6 * (\<Sum>i < n + 1. i^Suc (Suc 0)) = n * (n + 1) * (2 * n + 1)"
   (is "?P n" is "?S n = _")
 proof (induct n)
   show "?P 0" by simp
 next
-  fix n have "?S (n + 1) = ?S n + # 6 * (n + 1)^Suc (Suc 0)" by (simp add: distrib)
-  also assume "?S n = n * (n + 1) * (# 2 * n + 1)"
-  also have "... + # 6 * (n + 1)^Suc (Suc 0) =
-    (n + 1) * (n + # 2) * (# 2 * (n + 1) + 1)" by (simp add: distrib)
+  fix n have "?S (n + 1) = ?S n + 6 * (n + 1)^Suc (Suc 0)" by (simp add: distrib)
+  also assume "?S n = n * (n + 1) * (2 * n + 1)"
+  also have "... + 6 * (n + 1)^Suc (Suc 0) =
+    (n + 1) * (n + 2) * (2 * (n + 1) + 1)" by (simp add: distrib)
   finally show "?P (Suc n)" by simp
 qed
 
 theorem sum_of_cubes:
-  "# 4 * (\<Sum>i < n + 1. i^# 3) = (n * (n + 1))^Suc (Suc 0)"
+  "4 * (\<Sum>i < n + 1. i^3) = (n * (n + 1))^Suc (Suc 0)"
   (is "?P n" is "?S n = _")
 proof (induct n)
   show "?P 0" by (simp add: power_eq_if)
 next
-  fix n have "?S (n + 1) = ?S n + # 4 * (n + 1)^# 3"
+  fix n have "?S (n + 1) = ?S n + 4 * (n + 1)^3"
     by (simp add: power_eq_if distrib)
   also assume "?S n = (n * (n + 1))^Suc (Suc 0)"
-  also have "... + # 4 * (n + 1)^# 3 = ((n + 1) * ((n + 1) + 1))^Suc (Suc 0)"
+  also have "... + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^Suc (Suc 0)"
     by (simp add: power_eq_if distrib)
   finally show "?P (Suc n)" by simp
 qed
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/Lambda/Type.thy
--- a/src/HOL/Lambda/Type.thy	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Lambda/Type.thy	Sat Oct 06 00:02:46 2001 +0200
@@ -59,11 +59,11 @@
 
 subsection {* Some examples *}
 
-lemma "e |- Abs (Abs (Abs (Var 1 $ (Var # 2 $ Var 1 $ Var 0)))) : ?T"
+lemma "e |- Abs (Abs (Abs (Var 1 $ (Var 2 $ Var 1 $ Var 0)))) : ?T"
   apply force
   done
 
-lemma "e |- Abs (Abs (Abs (Var # 2 $ Var 0 $ (Var 1 $ Var 0)))) : ?T"
+lemma "e |- Abs (Abs (Abs (Var 2 $ Var 0 $ (Var 1 $ Var 0)))) : ?T"
   apply force
   done
 
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Library/While_Combinator.thy	Sat Oct 06 00:02:46 2001 +0200
@@ -135,14 +135,14 @@
  theory.}
 *}
 
-theorem "P (lfp (\<lambda>N::int set. {Numeral0} \<union> {(n + # 2) mod # 6 | n. n \<in> N})) =
-    P {Numeral0, # 4, # 2}"
+theorem "P (lfp (\<lambda>N::int set. {Numeral0} \<union> {(n + 2) mod 6 | n. n \<in> N})) =
+    P {Numeral0, 4, 2}"
 proof -
   have aux: "!!f A B. {f n | n. A n \<or> B n} = {f n | n. A n} \<union> {f n | n. B n}"
     apply blast
     done
   show ?thesis
-    apply (subst lfp_conv_while [where ?U = "{Numeral0, Numeral1, # 2, # 3, # 4, # 5}"])
+    apply (subst lfp_conv_while [where ?U = "{Numeral0, Numeral1, 2, 3, 4, 5}"])
        apply (rule monoI)
       apply blast
      apply simp
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/NumberTheory/EulerFermat.thy
--- a/src/HOL/NumberTheory/EulerFermat.thy	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/NumberTheory/EulerFermat.thy	Sat Oct 06 00:02:46 2001 +0200
@@ -55,7 +55,7 @@
   zcongm :: "int => int => int => bool"
   "zcongm m == \<lambda>a b. zcong a b m"
 
-lemma abs_eq_1_iff [iff]: "(abs z = (Numeral1::int)) = (z = Numeral1 \<or> z = # -1)"
+lemma abs_eq_1_iff [iff]: "(abs z = (Numeral1::int)) = (z = Numeral1 \<or> z = -1)"
   -- {* LCP: not sure why this lemma is needed now *}
   apply (auto simp add: zabs_def)
   done
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/NumberTheory/Fib.thy
--- a/src/HOL/NumberTheory/Fib.thy	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/NumberTheory/Fib.thy	Sat Oct 06 00:02:46 2001 +0200
@@ -67,14 +67,14 @@
 *}
 
 lemma fib_Cassini: "int (fib (Suc (Suc n)) * fib n) =
-  (if n mod # 2 = 0 then int (fib (Suc n) * fib (Suc n)) - Numeral1
+  (if n mod 2 = 0 then int (fib (Suc n) * fib (Suc n)) - Numeral1
    else int (fib (Suc n) * fib (Suc n)) + Numeral1)"
   apply (induct n rule: fib.induct)
     apply (simp add: fib.Suc_Suc)
    apply (simp add: fib.Suc_Suc mod_Suc)
   apply (simp add: fib.Suc_Suc
     add_mult_distrib add_mult_distrib2 mod_Suc zmult_int [symmetric] zmult_ac)
-  apply (subgoal_tac "x mod # 2 < # 2", arith)
+  apply (subgoal_tac "x mod 2 < 2", arith)
   apply simp
   done
 
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/NumberTheory/WilsonBij.thy
--- a/src/HOL/NumberTheory/WilsonBij.thy	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/NumberTheory/WilsonBij.thy	Sat Oct 06 00:02:46 2001 +0200
@@ -133,15 +133,15 @@
   apply auto
   done
 
-lemma aux3: "x \<le> p - # 2 ==> x < (p::int)"
+lemma aux3: "x \<le> p - 2 ==> x < (p::int)"
   apply auto
   done
 
-lemma aux4: "x \<le> p - # 2 ==> x < (p::int)-Numeral1"
+lemma aux4: "x \<le> p - 2 ==> x < (p::int)-Numeral1"
   apply auto
   done
 
-lemma inv_inj: "p \<in> zprime ==> inj_on (inv p) (d22set (p - # 2))"
+lemma inv_inj: "p \<in> zprime ==> inj_on (inv p) (d22set (p - 2))"
   apply (unfold inj_on_def)
   apply auto
   apply (rule zcong_zless_imp_eq)
@@ -160,7 +160,7 @@
   done
 
 lemma inv_d22set_d22set:
-    "p \<in> zprime ==> inv p ` d22set (p - # 2) = d22set (p - # 2)"
+    "p \<in> zprime ==> inv p ` d22set (p - 2) = d22set (p - 2)"
   apply (rule endo_inj_surj)
     apply (rule d22set_fin)
    apply (erule_tac [2] inv_inj)
@@ -173,9 +173,9 @@
   done
 
 lemma d22set_d22set_bij:
-    "p \<in> zprime ==> (d22set (p - # 2), d22set (p - # 2)) \<in> bijR (reciR p)"
+    "p \<in> zprime ==> (d22set (p - 2), d22set (p - 2)) \<in> bijR (reciR p)"
   apply (unfold reciR_def)
-  apply (rule_tac s = "(d22set (p - # 2), inv p ` d22set (p - # 2))" in subst)
+  apply (rule_tac s = "(d22set (p - 2), inv p ` d22set (p - 2))" in subst)
    apply (simp add: inv_d22set_d22set)
   apply (rule inj_func_bijR)
     apply (rule_tac [3] d22set_fin)
@@ -187,7 +187,7 @@
          apply (auto intro: d22set_g_1 d22set_le aux2 aux3 aux4)
   done
 
-lemma reciP_bijP: "p \<in> zprime ==> bijP (reciR p) (d22set (p - # 2))"
+lemma reciP_bijP: "p \<in> zprime ==> bijP (reciR p) (d22set (p - 2))"
   apply (unfold reciR_def bijP_def)
   apply auto
   apply (rule d22set_mem)
@@ -217,7 +217,7 @@
   apply auto
   done
 
-lemma bijER_d22set: "p \<in> zprime ==> d22set (p - # 2) \<in> bijER (reciR p)"
+lemma bijER_d22set: "p \<in> zprime ==> d22set (p - 2) \<in> bijER (reciR p)"
   apply (rule bijR_bijER)
      apply (erule d22set_d22set_bij)
     apply (erule reciP_bijP)
@@ -245,12 +245,12 @@
    apply auto
   done
 
-theorem Wilson_Bij: "p \<in> zprime ==> [zfact (p - Numeral1) = # -1] (mod p)"
-  apply (subgoal_tac "zcong ((p - Numeral1) * zfact (p - # 2)) (# -1 * Numeral1) p")
+theorem Wilson_Bij: "p \<in> zprime ==> [zfact (p - Numeral1) = -1] (mod p)"
+  apply (subgoal_tac "zcong ((p - Numeral1) * zfact (p - 2)) (-1 * Numeral1) p")
    apply (rule_tac [2] zcong_zmult)
     apply (simp add: zprime_def)
     apply (subst zfact.simps)
-    apply (rule_tac t = "p - Numeral1 - Numeral1" and s = "p - # 2" in subst)
+    apply (rule_tac t = "p - Numeral1 - Numeral1" and s = "p - 2" in subst)
      apply auto
    apply (simp add: zcong_def)
   apply (subst d22set_prod_zfact [symmetric])
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/NumberTheory/WilsonRuss.thy
--- a/src/HOL/NumberTheory/WilsonRuss.thy	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/NumberTheory/WilsonRuss.thy	Sat Oct 06 00:02:46 2001 +0200
@@ -20,7 +20,7 @@
   wset :: "int * int => int set"
 
 defs
-  inv_def: "inv p a == (a^(nat (p - # 2))) mod p"
+  inv_def: "inv p a == (a^(nat (p - 2))) mod p"
 
 recdef wset
   "measure ((\<lambda>(a, p). nat a) :: int * int => nat)"
@@ -32,7 +32,7 @@
 
 text {* \medskip @{term [source] inv} *}
 
-lemma aux: "Numeral1 < m ==> Suc (nat (m - # 2)) = nat (m - Numeral1)"
+lemma aux: "Numeral1 < m ==> Suc (nat (m - 2)) = nat (m - Numeral1)"
   apply (subst int_int_eq [symmetric])
   apply auto
   done
@@ -137,8 +137,8 @@
   apply (simp add: pos_mod_bound)
   done
 
-lemma aux: "# 5 \<le> p ==>
-    nat (p - # 2) * nat (p - # 2) = Suc (nat (p - Numeral1) * nat (p - # 3))"
+lemma aux: "5 \<le> p ==>
+    nat (p - 2) * nat (p - 2) = Suc (nat (p - Numeral1) * nat (p - 3))"
   apply (subst int_int_eq [symmetric])
   apply (simp add: zmult_int [symmetric])
   apply (simp add: zdiff_zmult_distrib zdiff_zmult_distrib2)
@@ -154,7 +154,7 @@
   done
 
 lemma inv_inv: "p \<in> zprime \<Longrightarrow>
-    # 5 \<le> p \<Longrightarrow> Numeral0 < a \<Longrightarrow> a < p ==> inv p (inv p a) = a"
+    5 \<le> p \<Longrightarrow> Numeral0 < a \<Longrightarrow> a < p ==> inv p (inv p a) = a"
   apply (unfold inv_def)
   apply (subst zpower_zmod)
   apply (subst zpower_zpower)
@@ -165,7 +165,7 @@
       apply (subst zcong_zmod [symmetric])
       apply (subst aux)
        apply (subgoal_tac [2]
-	 "zcong (a * a^(nat (p - Numeral1) * nat (p - # 3))) (a * Numeral1) p")
+	 "zcong (a * a^(nat (p - Numeral1) * nat (p - 3))) (a * Numeral1) p")
         apply (rule_tac [3] zcong_zmult)
          apply (rule_tac [4] zcong_zpower_zmult)
          apply (erule_tac [4] Little_Fermat)
@@ -256,7 +256,7 @@
   done
 
 lemma wset_mem_inv_mem [rule_format]:
-  "p \<in> zprime --> # 5 \<le> p --> a < p - Numeral1 --> b \<in> wset (a, p)
+  "p \<in> zprime --> 5 \<le> p --> a < p - Numeral1 --> b \<in> wset (a, p)
     --> inv p b \<in> wset (a, p)"
   apply (induct a p rule: wset_induct)
    apply auto
@@ -274,7 +274,7 @@
   done
 
 lemma wset_inv_mem_mem:
-  "p \<in> zprime \<Longrightarrow> # 5 \<le> p \<Longrightarrow> a < p - Numeral1 \<Longrightarrow> Numeral1 < b \<Longrightarrow> b < p - Numeral1
+  "p \<in> zprime \<Longrightarrow> 5 \<le> p \<Longrightarrow> a < p - Numeral1 \<Longrightarrow> Numeral1 < b \<Longrightarrow> b < p - Numeral1
     \<Longrightarrow> inv p b \<in> wset (a, p) \<Longrightarrow> b \<in> wset (a, p)"
   apply (rule_tac s = "inv p (inv p b)" and t = b in subst)
    apply (rule_tac [2] wset_mem_inv_mem)
@@ -292,7 +292,7 @@
 
 lemma wset_zcong_prod_1 [rule_format]:
   "p \<in> zprime -->
-    # 5 \<le> p --> a < p - Numeral1 --> [setprod (wset (a, p)) = Numeral1] (mod p)"
+    5 \<le> p --> a < p - Numeral1 --> [setprod (wset (a, p)) = Numeral1] (mod p)"
   apply (induct a p rule: wset_induct)
    prefer 2
    apply (subst wset.simps)
@@ -314,7 +314,7 @@
     apply auto
   done
 
-lemma d22set_eq_wset: "p \<in> zprime ==> d22set (p - # 2) = wset (p - # 2, p)"
+lemma d22set_eq_wset: "p \<in> zprime ==> d22set (p - 2) = wset (p - 2, p)"
   apply safe
    apply (erule wset_mem)
      apply (rule_tac [2] d22set_g_1)
@@ -323,7 +323,7 @@
       apply (erule_tac [4] wset_g_1)
        prefer 6
        apply (subst zle_add1_eq_le [symmetric])
-       apply (subgoal_tac "p - # 2 + Numeral1 = p - Numeral1")
+       apply (subgoal_tac "p - 2 + Numeral1 = p - Numeral1")
         apply (simp (no_asm_simp))
         apply (erule wset_less)
          apply auto
@@ -332,36 +332,36 @@
 
 subsection {* Wilson *}
 
-lemma prime_g_5: "p \<in> zprime \<Longrightarrow> p \<noteq> # 2 \<Longrightarrow> p \<noteq> # 3 ==> # 5 \<le> p"
+lemma prime_g_5: "p \<in> zprime \<Longrightarrow> p \<noteq> 2 \<Longrightarrow> p \<noteq> 3 ==> 5 \<le> p"
   apply (unfold zprime_def dvd_def)
-  apply (case_tac "p = # 4")
+  apply (case_tac "p = 4")
    apply auto
    apply (rule notE)
     prefer 2
     apply assumption
    apply (simp (no_asm))
-   apply (rule_tac x = "# 2" in exI)
+   apply (rule_tac x = "2" in exI)
    apply safe
-     apply (rule_tac x = "# 2" in exI)
+     apply (rule_tac x = "2" in exI)
      apply auto
   apply arith
   done
 
 theorem Wilson_Russ:
-    "p \<in> zprime ==> [zfact (p - Numeral1) = # -1] (mod p)"
-  apply (subgoal_tac "[(p - Numeral1) * zfact (p - # 2) = # -1 * Numeral1] (mod p)")
+    "p \<in> zprime ==> [zfact (p - Numeral1) = -1] (mod p)"
+  apply (subgoal_tac "[(p - Numeral1) * zfact (p - 2) = -1 * Numeral1] (mod p)")
    apply (rule_tac [2] zcong_zmult)
     apply (simp only: zprime_def)
     apply (subst zfact.simps)
-    apply (rule_tac t = "p - Numeral1 - Numeral1" and s = "p - # 2" in subst)
+    apply (rule_tac t = "p - Numeral1 - Numeral1" and s = "p - 2" in subst)
      apply auto
    apply (simp only: zcong_def)
    apply (simp (no_asm_simp))
-  apply (case_tac "p = # 2")
+  apply (case_tac "p = 2")
    apply (simp add: zfact.simps)
-  apply (case_tac "p = # 3")
+  apply (case_tac "p = 3")
    apply (simp add: zfact.simps)
-  apply (subgoal_tac "# 5 \<le> p")
+  apply (subgoal_tac "5 \<le> p")
    apply (erule_tac [2] prime_g_5)
     apply (subst d22set_prod_zfact [symmetric])
     apply (subst d22set_eq_wset)
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/Numeral.thy
--- a/src/HOL/Numeral.thy	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Numeral.thy	Sat Oct 06 00:02:46 2001 +0200
@@ -24,7 +24,7 @@
 
 syntax
   "_constify" :: "num => numeral"    ("_")
-  "_Numeral" :: "numeral => 'a"    ("#_")
+  "_Numeral" :: "numeral => 'a"    ("_")
   Numeral0 :: 'a
   Numeral1 :: 'a
 
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/Real/HahnBanach/VectorSpace.thy
--- a/src/HOL/Real/HahnBanach/VectorSpace.thy	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Real/HahnBanach/VectorSpace.thy	Sat Oct 06 00:02:46 2001 +0200
@@ -86,7 +86,7 @@
   by (unfold is_vectorspace_def) simp
 
 lemma negate_eq2a:
-  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> # -1 \<cdot> x = - x"
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> -1 \<cdot> x = - x"
   by (unfold is_vectorspace_def) simp
 
 lemma diff_eq2:
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/Real/RComplete.ML
--- a/src/HOL/Real/RComplete.ML	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Real/RComplete.ML	Sat Oct 06 00:02:46 2001 +0200
@@ -8,7 +8,7 @@
 
 claset_ref() := claset() delWrapper "bspec";
 
-Goal "x/# 2 + x/# 2 = (x::real)";
+Goal "x/2 + x/2 = (x::real)";
 by (Simp_tac 1);
 qed "real_sum_of_halves";
 
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/Real/RealArith0.ML
--- a/src/HOL/Real/RealArith0.ML	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Real/RealArith0.ML	Sat Oct 06 00:02:46 2001 +0200
@@ -276,34 +276,34 @@
 set trace_simp;
 fun test s = (Goal s; by (Simp_tac 1)); 
 
-test "Numeral0 <= (y::real) * # -2";
-test "# 9*x = # 12 * (y::real)";
-test "(# 9*x) / (# 12 * (y::real)) = z";
-test "# 9*x < # 12 * (y::real)";
-test "# 9*x <= # 12 * (y::real)";
+test "Numeral0 <= (y::real) * -2";
+test "9*x = 12 * (y::real)";
+test "(9*x) / (12 * (y::real)) = z";
+test "9*x < 12 * (y::real)";
+test "9*x <= 12 * (y::real)";
 
-test "# -99*x = # 132 * (y::real)";
-test "(# -99*x) / (# 132 * (y::real)) = z";
-test "# -99*x < # 132 * (y::real)";
-test "# -99*x <= # 132 * (y::real)";
+test "-99*x = 132 * (y::real)";
+test "(-99*x) / (132 * (y::real)) = z";
+test "-99*x < 132 * (y::real)";
+test "-99*x <= 132 * (y::real)";
 
-test "# 999*x = # -396 * (y::real)";
-test "(# 999*x) / (# -396 * (y::real)) = z";
-test "# 999*x < # -396 * (y::real)";
-test "# 999*x <= # -396 * (y::real)";
+test "999*x = -396 * (y::real)";
+test "(999*x) / (-396 * (y::real)) = z";
+test "999*x < -396 * (y::real)";
+test "999*x <= -396 * (y::real)";
 
-test "# -99*x = # -81 * (y::real)";
-test "(# -99*x) / (# -81 * (y::real)) = z";
-test "# -99*x <= # -81 * (y::real)";
-test "# -99*x < # -81 * (y::real)";
+test "-99*x = -81 * (y::real)";
+test "(-99*x) / (-81 * (y::real)) = z";
+test "-99*x <= -81 * (y::real)";
+test "-99*x < -81 * (y::real)";
 
-test "# -2 * x = # -1 * (y::real)";
-test "# -2 * x = -(y::real)";
-test "(# -2 * x) / (# -1 * (y::real)) = z";
-test "# -2 * x < -(y::real)";
-test "# -2 * x <= # -1 * (y::real)";
-test "-x < # -23 * (y::real)";
-test "-x <= # -23 * (y::real)";
+test "-2 * x = -1 * (y::real)";
+test "-2 * x = -(y::real)";
+test "(-2 * x) / (-1 * (y::real)) = z";
+test "-2 * x < -(y::real)";
+test "-2 * x <= -1 * (y::real)";
+test "-x < -23 * (y::real)";
+test "-x <= -23 * (y::real)";
 *)
 
 
@@ -505,18 +505,18 @@
 qed "real_divide_1";
 Addsimps [real_divide_1];
 
-Goal "x/# -1 = -(x::real)";
+Goal "x/-1 = -(x::real)";
 by (Simp_tac 1); 
 qed "real_divide_minus1";
 Addsimps [real_divide_minus1];
 
-Goal "# -1/(x::real) = - (Numeral1/x)";
+Goal "-1/(x::real) = - (Numeral1/x)";
 by (simp_tac (simpset() addsimps [real_divide_def, real_minus_inverse]) 1); 
 qed "real_minus1_divide";
 Addsimps [real_minus1_divide];
 
 Goal "[| (Numeral0::real) < d1; Numeral0 < d2 |] ==> EX e. Numeral0 < e & e < d1 & e < d2";
-by (res_inst_tac [("x","(min d1 d2)/# 2")] exI 1); 
+by (res_inst_tac [("x","(min d1 d2)/2")] exI 1); 
 by (asm_simp_tac (simpset() addsimps [min_def]) 1); 
 qed "real_lbound_gt_zero";
 
@@ -647,11 +647,11 @@
 
 (*** Density of the Reals ***)
 
-Goal "x < y ==> x < (x+y) / (# 2::real)";
+Goal "x < y ==> x < (x+y) / (2::real)";
 by Auto_tac;
 qed "real_less_half_sum";
 
-Goal "x < y ==> (x+y)/(# 2::real) < y";
+Goal "x < y ==> (x+y)/(2::real) < y";
 by Auto_tac;
 qed "real_gt_half_sum";
 
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/Real/RealBin.ML
--- a/src/HOL/Real/RealBin.ML	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Real/RealBin.ML	Sat Oct 06 00:02:46 2001 +0200
@@ -58,18 +58,18 @@
 
 Addsimps [mult_real_number_of];
 
-Goal "(# 2::real) = Numeral1 + Numeral1";
+Goal "(2::real) = Numeral1 + Numeral1";
 by (Simp_tac 1);
 val lemma = result();
 
 (*For specialist use: NOT as default simprules*)
-Goal "# 2 * z = (z+z::real)";
+Goal "2 * z = (z+z::real)";
 by (simp_tac (simpset ()
 	      addsimps [lemma, real_add_mult_distrib,
 			one_eq_numeral_1 RS sym]) 1);
 qed "real_mult_2";
 
-Goal "z * # 2 = (z+z::real)";
+Goal "z * 2 = (z+z::real)";
 by (stac real_mult_commute 1 THEN rtac real_mult_2 1);
 qed "real_mult_2_right";
 
@@ -111,12 +111,12 @@
 
 (*** New versions of existing theorems involving 0, 1r ***)
 
-Goal "- Numeral1 = (# -1::real)";
+Goal "- Numeral1 = (-1::real)";
 by (Simp_tac 1);
 qed "minus_numeral_one";
 
 
-(*Maps 0 to Numeral0 and 1r to Numeral1 and -1r to # -1*)
+(*Maps 0 to Numeral0 and 1r to Numeral1 and -1r to -1*)
 val real_numeral_ss = 
     HOL_ss addsimps [zero_eq_numeral_0, one_eq_numeral_1, 
 		     minus_numeral_one];
@@ -488,7 +488,7 @@
 structure CombineNumeralsData =
   struct
   val add		= op + : int*int -> int 
-  val mk_sum    	= long_mk_sum    (*to work for e.g. # 2*x + # 3*x *)
+  val mk_sum    	= long_mk_sum    (*to work for e.g. 2*x + 3*x *)
   val dest_sum		= dest_sum
   val mk_coeff		= mk_coeff
   val dest_coeff	= dest_coeff 1
@@ -548,35 +548,35 @@
 set trace_simp;
 fun test s = (Goal s; by (Simp_tac 1)); 
 
-test "l + # 2 + # 2 + # 2 + (l + # 2) + (oo + # 2) = (uu::real)";
+test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::real)";
 
-test "# 2*u = (u::real)";
-test "(i + j + # 12 + (k::real)) - # 15 = y";
-test "(i + j + # 12 + (k::real)) - # 5 = y";
+test "2*u = (u::real)";
+test "(i + j + 12 + (k::real)) - 15 = y";
+test "(i + j + 12 + (k::real)) - 5 = y";
 
 test "y - b < (b::real)";
-test "y - (# 3*b + c) < (b::real) - # 2*c";
+test "y - (3*b + c) < (b::real) - 2*c";
 
-test "(# 2*x - (u*v) + y) - v*# 3*u = (w::real)";
-test "(# 2*x*u*v + (u*v)*# 4 + y) - v*u*# 4 = (w::real)";
-test "(# 2*x*u*v + (u*v)*# 4 + y) - v*u = (w::real)";
-test "u*v - (x*u*v + (u*v)*# 4 + y) = (w::real)";
+test "(2*x - (u*v) + y) - v*3*u = (w::real)";
+test "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::real)";
+test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::real)";
+test "u*v - (x*u*v + (u*v)*4 + y) = (w::real)";
 
-test "(i + j + # 12 + (k::real)) = u + # 15 + y";
-test "(i + j*# 2 + # 12 + (k::real)) = j + # 5 + y";
+test "(i + j + 12 + (k::real)) = u + 15 + y";
+test "(i + j*2 + 12 + (k::real)) = j + 5 + y";
 
-test "# 2*y + # 3*z + # 6*w + # 2*y + # 3*z + # 2*u = # 2*y' + # 3*z' + # 6*w' + # 2*y' + # 3*z' + u + (vv::real)";
+test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + (vv::real)";
 
 test "a + -(b+c) + b = (d::real)";
 test "a + -(b+c) - b = (d::real)";
 
 (*negative numerals*)
-test "(i + j + # -2 + (k::real)) - (u + # 5 + y) = zz";
-test "(i + j + # -3 + (k::real)) < u + # 5 + y";
-test "(i + j + # 3 + (k::real)) < u + # -6 + y";
-test "(i + j + # -12 + (k::real)) - # 15 = y";
-test "(i + j + # 12 + (k::real)) - # -15 = y";
-test "(i + j + # -12 + (k::real)) - # -15 = y";
+test "(i + j + -2 + (k::real)) - (u + 5 + y) = zz";
+test "(i + j + -3 + (k::real)) < u + 5 + y";
+test "(i + j + 3 + (k::real)) < u + -6 + y";
+test "(i + j + -12 + (k::real)) - 15 = y";
+test "(i + j + 12 + (k::real)) - -15 = y";
+test "(i + j + -12 + (k::real)) - -15 = y";
 *)
 
 
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/Real/RealPow.ML
--- a/src/HOL/Real/RealPow.ML	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Real/RealPow.ML	Sat Oct 06 00:02:46 2001 +0200
@@ -76,7 +76,7 @@
 qed "realpow_eq_one";
 Addsimps [realpow_eq_one];
 
-Goal "abs((# -1) ^ n) = (Numeral1::real)";
+Goal "abs((-1) ^ n) = (Numeral1::real)";
 by (induct_tac "n" 1);
 by (auto_tac (claset(), simpset() addsimps [abs_mult]));
 qed "abs_realpow_minus_one";
@@ -127,13 +127,13 @@
 by (auto_tac (claset() addDs [realpow_ge_one], simpset()));
 qed "realpow_ge_one2";
 
-Goal "(Numeral1::real) <= # 2 ^ n";
+Goal "(Numeral1::real) <= 2 ^ n";
 by (res_inst_tac [("y","Numeral1 ^ n")] order_trans 1);
 by (rtac realpow_le 2);
 by (auto_tac (claset() addIs [order_less_imp_le], simpset()));
 qed "two_realpow_ge_one";
 
-Goal "real (n::nat) < # 2 ^ n";
+Goal "real (n::nat) < 2 ^ n";
 by (induct_tac "n" 1);
 by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc]));
 by (stac real_mult_2 1);
@@ -142,18 +142,18 @@
 qed "two_realpow_gt";
 Addsimps [two_realpow_gt,two_realpow_ge_one];
 
-Goal "(# -1) ^ (# 2*n) = (Numeral1::real)";
+Goal "(-1) ^ (2*n) = (Numeral1::real)";
 by (induct_tac "n" 1);
 by Auto_tac;
 qed "realpow_minus_one";
 Addsimps [realpow_minus_one];
 
-Goal "(# -1) ^ Suc (# 2*n) = -(Numeral1::real)";
+Goal "(-1) ^ Suc (2*n) = -(Numeral1::real)";
 by Auto_tac;
 qed "realpow_minus_one_odd";
 Addsimps [realpow_minus_one_odd];
 
-Goal "(# -1) ^ Suc (Suc (# 2*n)) = (Numeral1::real)";
+Goal "(-1) ^ Suc (Suc (2*n)) = (Numeral1::real)";
 by Auto_tac;
 qed "realpow_minus_one_even";
 Addsimps [realpow_minus_one_even];
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/Real/ex/BinEx.thy
--- a/src/HOL/Real/ex/BinEx.thy	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Real/ex/BinEx.thy	Sat Oct 06 00:02:46 2001 +0200
@@ -15,52 +15,52 @@
 
 text {* \medskip Addition *}
 
-lemma "(# 1359::real) + # -2468 = # -1109"
+lemma "(1359::real) + -2468 = -1109"
   by simp
 
-lemma "(# 93746::real) + # -46375 = # 47371"
+lemma "(93746::real) + -46375 = 47371"
   by simp
 
 
 text {* \medskip Negation *}
 
-lemma "- (# 65745::real) = # -65745"
+lemma "- (65745::real) = -65745"
   by simp
 
-lemma "- (# -54321::real) = # 54321"
+lemma "- (-54321::real) = 54321"
   by simp
 
 
 text {* \medskip Multiplication *}
 
-lemma "(# -84::real) * # 51 = # -4284"
+lemma "(-84::real) * 51 = -4284"
   by simp
 
-lemma "(# 255::real) * # 255 = # 65025"
+lemma "(255::real) * 255 = 65025"
   by simp
 
-lemma "(# 1359::real) * # -2468 = # -3354012"
+lemma "(1359::real) * -2468 = -3354012"
   by simp
 
 
 text {* \medskip Inequalities *}
 
-lemma "(# 89::real) * # 10 \<noteq> # 889"
+lemma "(89::real) * 10 \<noteq> 889"
   by simp
 
-lemma "(# 13::real) < # 18 - # 4"
+lemma "(13::real) < 18 - 4"
   by simp
 
-lemma "(# -345::real) < # -242 + # -100"
+lemma "(-345::real) < -242 + -100"
   by simp
 
-lemma "(# 13557456::real) < # 18678654"
+lemma "(13557456::real) < 18678654"
   by simp
 
-lemma "(# 999999::real) \<le> (# 1000001 + Numeral1)-# 2"
+lemma "(999999::real) \<le> (1000001 + Numeral1) - 2"
   by simp
 
-lemma "(# 1234567::real) \<le> # 1234567"
+lemma "(1234567::real) \<le> 1234567"
   by simp
 
 
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/Real/ex/Sqrt_Irrational.thy
--- a/src/HOL/Real/ex/Sqrt_Irrational.thy	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Real/ex/Sqrt_Irrational.thy	Sat Oct 06 00:02:46 2001 +0200
@@ -114,15 +114,15 @@
   this formally :-).
 *}
 
-theorem "x\<twosuperior> = real (# 2::nat) ==> x \<notin> \<rat>"
+theorem "x\<twosuperior> = real (2::nat) ==> x \<notin> \<rat>"
 proof (rule sqrt_prime_irrational)
   {
-    fix m :: nat assume dvd: "m dvd # 2"
-    hence "m \<le> # 2" by (simp add: dvd_imp_le)
+    fix m :: nat assume dvd: "m dvd 2"
+    hence "m \<le> 2" by (simp add: dvd_imp_le)
     moreover from dvd have "m \<noteq> 0" by (auto dest: dvd_0_left iff del: neq0_conv)
-    ultimately have "m = 1 \<or> m = # 2" by arith
+    ultimately have "m = 1 \<or> m = 2" by arith
   }
-  thus "# 2 \<in> prime" by (simp add: prime_def)
+  thus "2 \<in> prime" by (simp add: prime_def)
 qed
 
 text {*
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/Real/real_arith0.ML
--- a/src/HOL/Real/real_arith0.ML	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Real/real_arith0.ML	Sat Oct 06 00:02:46 2001 +0200
@@ -118,7 +118,7 @@
 qed "";
 
 Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
-\     ==> # 6*a <= # 5*l+i";
+\     ==> 6*a <= 5*l+i";
 by (fast_arith_tac 1);
 qed "";
 *)
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/UNITY/Simple/Mutex.ML
--- a/src/HOL/UNITY/Simple/Mutex.ML	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/UNITY/Simple/Mutex.ML	Sat Oct 06 00:02:46 2001 +0200
@@ -25,7 +25,7 @@
 qed "IV";
 
 (*The safety property: mutual exclusion*)
-Goal "Mutex : Always {s. ~ (m s = # 3 & n s = # 3)}";
+Goal "Mutex : Always {s. ~ (m s = 3 & n s = 3)}";
 by (rtac ([IU, IV] MRS Always_Int_I RS Always_weaken) 1);
 by Auto_tac;
 qed "mutual_exclusion";
@@ -42,33 +42,33 @@
 getgoal 1;  
 
 
-Goal "((Numeral1::int) <= i & i <= # 3) = (i = Numeral1 | i = # 2 | i = # 3)";
+Goal "((Numeral1::int) <= i & i <= 3) = (i = Numeral1 | i = 2 | i = 3)";
 by (arith_tac 1);
 qed "eq_123";
 
 
 (*** Progress for U ***)
 
-Goalw [Unless_def] "Mutex : {s. m s=# 2} Unless {s. m s=# 3}";
+Goalw [Unless_def] "Mutex : {s. m s=2} Unless {s. m s=3}";
 by (constrains_tac 1);
 qed "U_F0";
 
-Goal "Mutex : {s. m s=Numeral1} LeadsTo {s. p s = v s & m s = # 2}";
+Goal "Mutex : {s. m s=Numeral1} LeadsTo {s. p s = v s & m s = 2}";
 by (ensures_tac "U1" 1);
 qed "U_F1";
 
-Goal "Mutex : {s. ~ p s & m s = # 2} LeadsTo {s. m s = # 3}";
+Goal "Mutex : {s. ~ p s & m s = 2} LeadsTo {s. m s = 3}";
 by (cut_facts_tac [IU] 1);
 by (ensures_tac "U2" 1);
 qed "U_F2";
 
-Goal "Mutex : {s. m s = # 3} LeadsTo {s. p s}";
-by (res_inst_tac [("B", "{s. m s = # 4}")] LeadsTo_Trans 1);
+Goal "Mutex : {s. m s = 3} LeadsTo {s. p s}";
+by (res_inst_tac [("B", "{s. m s = 4}")] LeadsTo_Trans 1);
 by (ensures_tac "U4" 2);
 by (ensures_tac "U3" 1);
 qed "U_F3";
 
-Goal "Mutex : {s. m s = # 2} LeadsTo {s. p s}";
+Goal "Mutex : {s. m s = 2} LeadsTo {s. p s}";
 by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo] 
 	  MRS LeadsTo_Diff) 1);
 by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1);
@@ -80,7 +80,7 @@
 by (Blast_tac 1);
 val U_lemma1 = result();
 
-Goal "Mutex : {s. Numeral1 <= m s & m s <= # 3} LeadsTo {s. p s}";
+Goal "Mutex : {s. Numeral1 <= m s & m s <= 3} LeadsTo {s. p s}";
 by (simp_tac (simpset() addsimps [eq_123, Collect_disj_eq, LeadsTo_Un_distrib,
 				  U_lemma1, U_lemma2, U_F3] ) 1);
 val U_lemma123 = result();
@@ -95,26 +95,26 @@
 (*** Progress for V ***)
 
 
-Goalw [Unless_def] "Mutex : {s. n s=# 2} Unless {s. n s=# 3}";
+Goalw [Unless_def] "Mutex : {s. n s=2} Unless {s. n s=3}";
 by (constrains_tac 1);
 qed "V_F0";
 
-Goal "Mutex : {s. n s=Numeral1} LeadsTo {s. p s = (~ u s) & n s = # 2}";
+Goal "Mutex : {s. n s=Numeral1} LeadsTo {s. p s = (~ u s) & n s = 2}";
 by (ensures_tac "V1" 1);
 qed "V_F1";
 
-Goal "Mutex : {s. p s & n s = # 2} LeadsTo {s. n s = # 3}";
+Goal "Mutex : {s. p s & n s = 2} LeadsTo {s. n s = 3}";
 by (cut_facts_tac [IV] 1);
 by (ensures_tac "V2" 1);
 qed "V_F2";
 
-Goal "Mutex : {s. n s = # 3} LeadsTo {s. ~ p s}";
-by (res_inst_tac [("B", "{s. n s = # 4}")] LeadsTo_Trans 1);
+Goal "Mutex : {s. n s = 3} LeadsTo {s. ~ p s}";
+by (res_inst_tac [("B", "{s. n s = 4}")] LeadsTo_Trans 1);
 by (ensures_tac "V4" 2);
 by (ensures_tac "V3" 1);
 qed "V_F3";
 
-Goal "Mutex : {s. n s = # 2} LeadsTo {s. ~ p s}";
+Goal "Mutex : {s. n s = 2} LeadsTo {s. ~ p s}";
 by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo] 
 	  MRS LeadsTo_Diff) 1);
 by (rtac ([V_F2, V_F3] MRS LeadsTo_Trans) 1);
@@ -126,7 +126,7 @@
 by (Blast_tac 1);
 val V_lemma1 = result();
 
-Goal "Mutex : {s. Numeral1 <= n s & n s <= # 3} LeadsTo {s. ~ p s}";
+Goal "Mutex : {s. Numeral1 <= n s & n s <= 3} LeadsTo {s. ~ p s}";
 by (simp_tac (simpset() addsimps [eq_123, Collect_disj_eq, LeadsTo_Un_distrib,
 				  V_lemma1, V_lemma2, V_F3] ) 1);
 val V_lemma123 = result();
@@ -142,7 +142,7 @@
 (** Absence of starvation **)
 
 (*Misra's F6*)
-Goal "Mutex : {s. m s = Numeral1} LeadsTo {s. m s = # 3}";
+Goal "Mutex : {s. m s = Numeral1} LeadsTo {s. m s = 3}";
 by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1);
 by (rtac U_F2 2);
 by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
@@ -154,7 +154,7 @@
 qed "m1_Leadsto_3";
 
 (*The same for V*)
-Goal "Mutex : {s. n s = Numeral1} LeadsTo {s. n s = # 3}";
+Goal "Mutex : {s. n s = Numeral1} LeadsTo {s. n s = 3}";
 by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1);
 by (rtac V_F2 2);
 by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/UNITY/Simple/Mutex.thy
--- a/src/HOL/UNITY/Simple/Mutex.thy	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/UNITY/Simple/Mutex.thy	Sat Oct 06 00:02:46 2001 +0200
@@ -25,16 +25,16 @@
     "U0 == {(s,s'). s' = s (|u:=True, m:=Numeral1|) & m s = Numeral0}"
 
   U1 :: command
-    "U1 == {(s,s'). s' = s (|p:= v s, m:=# 2|) & m s = Numeral1}"
+    "U1 == {(s,s'). s' = s (|p:= v s, m:=2|) & m s = Numeral1}"
 
   U2 :: command
-    "U2 == {(s,s'). s' = s (|m:=# 3|) & ~ p s & m s = # 2}"
+    "U2 == {(s,s'). s' = s (|m:=3|) & ~ p s & m s = 2}"
 
   U3 :: command
-    "U3 == {(s,s'). s' = s (|u:=False, m:=# 4|) & m s = # 3}"
+    "U3 == {(s,s'). s' = s (|u:=False, m:=4|) & m s = 3}"
 
   U4 :: command
-    "U4 == {(s,s'). s' = s (|p:=True, m:=Numeral0|) & m s = # 4}"
+    "U4 == {(s,s'). s' = s (|p:=True, m:=Numeral0|) & m s = 4}"
 
   (** The program for process V **)
   
@@ -42,16 +42,16 @@
     "V0 == {(s,s'). s' = s (|v:=True, n:=Numeral1|) & n s = Numeral0}"
 
   V1 :: command
-    "V1 == {(s,s'). s' = s (|p:= ~ u s, n:=# 2|) & n s = Numeral1}"
+    "V1 == {(s,s'). s' = s (|p:= ~ u s, n:=2|) & n s = Numeral1}"
 
   V2 :: command
-    "V2 == {(s,s'). s' = s (|n:=# 3|) & p s & n s = # 2}"
+    "V2 == {(s,s'). s' = s (|n:=3|) & p s & n s = 2}"
 
   V3 :: command
-    "V3 == {(s,s'). s' = s (|v:=False, n:=# 4|) & n s = # 3}"
+    "V3 == {(s,s'). s' = s (|v:=False, n:=4|) & n s = 3}"
 
   V4 :: command
-    "V4 == {(s,s'). s' = s (|p:=False, n:=Numeral0|) & n s = # 4}"
+    "V4 == {(s,s'). s' = s (|p:=False, n:=Numeral0|) & n s = 4}"
 
   Mutex :: state program
     "Mutex == mk_program ({s. ~ u s & ~ v s & m s = Numeral0 & n s = Numeral0},
@@ -62,15 +62,15 @@
   (** The correct invariants **)
 
   IU :: state set
-    "IU == {s. (u s = (Numeral1 <= m s & m s <= # 3)) & (m s = # 3 --> ~ p s)}"
+    "IU == {s. (u s = (Numeral1 <= m s & m s <= 3)) & (m s = 3 --> ~ p s)}"
 
   IV :: state set
-    "IV == {s. (v s = (Numeral1 <= n s & n s <= # 3)) & (n s = # 3 --> p s)}"
+    "IV == {s. (v s = (Numeral1 <= n s & n s <= 3)) & (n s = 3 --> p s)}"
 
   (** The faulty invariant (for U alone) **)
 
   bad_IU :: state set
-    "bad_IU == {s. (u s = (Numeral1 <= m s & m s <= # 3)) &
-	           (# 3 <= m s & m s <= # 4 --> ~ p s)}"
+    "bad_IU == {s. (u s = (Numeral1 <= m s & m s <= 3)) &
+	           (3 <= m s & m s <= 4 --> ~ p s)}"
 
 end
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/UNITY/Union.ML
--- a/src/HOL/UNITY/Union.ML	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/UNITY/Union.ML	Sat Oct 06 00:02:46 2001 +0200
@@ -352,7 +352,7 @@
 
 bind_thm ("ok_sym", ok_commute RS iffD1);
 
-Goal "OK {(Numeral0::int,F),(Numeral1,G),(# 2,H)} snd = (F ok G & (F Join G) ok H)";
+Goal "OK {(Numeral0::int,F),(Numeral1,G),(2,H)} snd = (F ok G & (F Join G) ok H)";
 by (asm_full_simp_tac
     (simpset() addsimps [Ball_def, conj_disj_distribR, ok_def, Join_def, 
                    OK_def, insert_absorb, all_conj_distrib, eq_commute]) 1); 
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/Unix/ROOT.ML
--- a/src/HOL/Unix/ROOT.ML	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Unix/ROOT.ML	Sat Oct 06 00:02:46 2001 +0200
@@ -1,3 +1,3 @@
 
-Library.setmp print_mode (! print_mode @ ["no_brackets"])
+Library.setmp print_mode (! print_mode @ ["no_brackets", "no_type_brackets"])
   use_thy "Unix";
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/arith_data.ML	Sat Oct 06 00:02:46 2001 +0200
@@ -438,7 +438,7 @@
   [Simplifier.change_simpset_of (op addSolver)
    (mk_solver "lin. arith." Fast_Arith.cut_lin_arith_tac),
   Simplifier.change_simpset_of (op addsimprocs) [fast_nat_arith_simproc],
-  Method.add_methods [("arith", (arith_method o # 2) oo Method.syntax Args.bang_facts,
+  Method.add_methods [("arith", (arith_method o #2) oo Method.syntax Args.bang_facts,
     "decide linear arithmethic")],
   Attrib.add_attributes [("arith_split",
     (Attrib.no_args arith_split_add, Attrib.no_args Attrib.undef_local_attribute),
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/ex/BinEx.thy
--- a/src/HOL/ex/BinEx.thy	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/ex/BinEx.thy	Sat Oct 06 00:02:46 2001 +0200
@@ -12,75 +12,75 @@
 
 text {* Addition *}
 
-lemma "(# 13::int) + # 19 = # 32"
+lemma "(13::int) + 19 = 32"
   by simp
 
-lemma "(# 1234::int) + # 5678 = # 6912"
+lemma "(1234::int) + 5678 = 6912"
   by simp
 
-lemma "(# 1359::int) + # -2468 = # -1109"
+lemma "(1359::int) + -2468 = -1109"
   by simp
 
-lemma "(# 93746::int) + # -46375 = # 47371"
+lemma "(93746::int) + -46375 = 47371"
   by simp
 
 
 text {* \medskip Negation *}
 
-lemma "- (# 65745::int) = # -65745"
+lemma "- (65745::int) = -65745"
   by simp
 
-lemma "- (# -54321::int) = # 54321"
+lemma "- (-54321::int) = 54321"
   by simp
 
 
 text {* \medskip Multiplication *}
 
-lemma "(# 13::int) * # 19 = # 247"
+lemma "(13::int) * 19 = 247"
   by simp
 
-lemma "(# -84::int) * # 51 = # -4284"
+lemma "(-84::int) * 51 = -4284"
   by simp
 
-lemma "(# 255::int) * # 255 = # 65025"
+lemma "(255::int) * 255 = 65025"
   by simp
 
-lemma "(# 1359::int) * # -2468 = # -3354012"
+lemma "(1359::int) * -2468 = -3354012"
   by simp
 
-lemma "(# 89::int) * # 10 \<noteq> # 889"
+lemma "(89::int) * 10 \<noteq> 889"
   by simp
 
-lemma "(# 13::int) < # 18 - # 4"
+lemma "(13::int) < 18 - 4"
   by simp
 
-lemma "(# -345::int) < # -242 + # -100"
+lemma "(-345::int) < -242 + -100"
   by simp
 
-lemma "(# 13557456::int) < # 18678654"
+lemma "(13557456::int) < 18678654"
   by simp
 
-lemma "(# 999999::int) \<le> (# 1000001 + Numeral1) - # 2"
+lemma "(999999::int) \<le> (1000001 + Numeral1) - 2"
   by simp
 
-lemma "(# 1234567::int) \<le> # 1234567"
+lemma "(1234567::int) \<le> 1234567"
   by simp
 
 
 text {* \medskip Quotient and Remainder *}
 
-lemma "(# 10::int) div # 3 = # 3"
+lemma "(10::int) div 3 = 3"
   by simp
 
-lemma "(# 10::int) mod # 3 = Numeral1"
+lemma "(10::int) mod 3 = Numeral1"
   by simp
 
 text {* A negative divisor *}
 
-lemma "(# 10::int) div # -3 = # -4"
+lemma "(10::int) div -3 = -4"
   by simp
 
-lemma "(# 10::int) mod # -3 = # -2"
+lemma "(10::int) mod -3 = -2"
   by simp
 
 text {*
@@ -88,50 +88,50 @@
   convention but not with the hardware of most computers}
 *}
 
-lemma "(# -10::int) div # 3 = # -4"
+lemma "(-10::int) div 3 = -4"
   by simp
 
-lemma "(# -10::int) mod # 3 = # 2"
+lemma "(-10::int) mod 3 = 2"
   by simp
 
 text {* A negative dividend \emph{and} divisor *}
 
-lemma "(# -10::int) div # -3 = # 3"
+lemma "(-10::int) div -3 = 3"
   by simp
 
-lemma "(# -10::int) mod # -3 = # -1"
+lemma "(-10::int) mod -3 = -1"
   by simp
 
 text {* A few bigger examples *}
 
-lemma "(# 8452::int) mod # 3 = Numeral1"
+lemma "(8452::int) mod 3 = Numeral1"
   by simp
 
-lemma "(# 59485::int) div # 434 = # 137"
+lemma "(59485::int) div 434 = 137"
   by simp
 
-lemma "(# 1000006::int) mod # 10 = # 6"
+lemma "(1000006::int) mod 10 = 6"
   by simp
 
 
 text {* \medskip Division by shifting *}
 
-lemma "# 10000000 div # 2 = (# 5000000::int)"
+lemma "10000000 div 2 = (5000000::int)"
   by simp
 
-lemma "# 10000001 mod # 2 = (Numeral1::int)"
+lemma "10000001 mod 2 = (Numeral1::int)"
   by simp
 
-lemma "# 10000055 div # 32 = (# 312501::int)"
+lemma "10000055 div 32 = (312501::int)"
   by simp
 
-lemma "# 10000055 mod # 32 = (# 23::int)"
+lemma "10000055 mod 32 = (23::int)"
   by simp
 
-lemma "# 100094 div # 144 = (# 695::int)"
+lemma "100094 div 144 = (695::int)"
   by simp
 
-lemma "# 100094 mod # 144 = (# 14::int)"
+lemma "100094 mod 144 = (14::int)"
   by simp
 
 
@@ -139,65 +139,65 @@
 
 text {* Successor *}
 
-lemma "Suc # 99999 = # 100000"
+lemma "Suc 99999 = 100000"
   by (simp add: Suc_nat_number_of)
     -- {* not a default rewrite since sometimes we want to have @{text "Suc #nnn"} *}
 
 
 text {* \medskip Addition *}
 
-lemma "(# 13::nat) + # 19 = # 32"
+lemma "(13::nat) + 19 = 32"
   by simp
 
-lemma "(# 1234::nat) + # 5678 = # 6912"
+lemma "(1234::nat) + 5678 = 6912"
   by simp
 
-lemma "(# 973646::nat) + # 6475 = # 980121"
+lemma "(973646::nat) + 6475 = 980121"
   by simp
 
 
 text {* \medskip Subtraction *}
 
-lemma "(# 32::nat) - # 14 = # 18"
+lemma "(32::nat) - 14 = 18"
   by simp
 
-lemma "(# 14::nat) - # 15 = Numeral0"
+lemma "(14::nat) - 15 = Numeral0"
   by simp
 
-lemma "(# 14::nat) - # 1576644 = Numeral0"
+lemma "(14::nat) - 1576644 = Numeral0"
   by simp
 
-lemma "(# 48273776::nat) - # 3873737 = # 44400039"
+lemma "(48273776::nat) - 3873737 = 44400039"
   by simp
 
 
 text {* \medskip Multiplication *}
 
-lemma "(# 12::nat) * # 11 = # 132"
+lemma "(12::nat) * 11 = 132"
   by simp
 
-lemma "(# 647::nat) * # 3643 = # 2357021"
+lemma "(647::nat) * 3643 = 2357021"
   by simp
 
 
 text {* \medskip Quotient and Remainder *}
 
-lemma "(# 10::nat) div # 3 = # 3"
+lemma "(10::nat) div 3 = 3"
   by simp
 
-lemma "(# 10::nat) mod # 3 = Numeral1"
+lemma "(10::nat) mod 3 = Numeral1"
   by simp
 
-lemma "(# 10000::nat) div # 9 = # 1111"
+lemma "(10000::nat) div 9 = 1111"
   by simp
 
-lemma "(# 10000::nat) mod # 9 = Numeral1"
+lemma "(10000::nat) mod 9 = Numeral1"
   by simp
 
-lemma "(# 10000::nat) div # 16 = # 625"
+lemma "(10000::nat) div 16 = 625"
   by simp
 
-lemma "(# 10000::nat) mod # 16 = Numeral0"
+lemma "(10000::nat) mod 16 = Numeral0"
   by simp
 
 
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/ex/NatSum.thy
--- a/src/HOL/ex/NatSum.thy	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/ex/NatSum.thy	Sat Oct 06 00:02:46 2001 +0200
@@ -36,8 +36,8 @@
 *}
 
 lemma sum_of_odd_squares:
-  "# 3 * setsum (\<lambda>i. Suc (i + i) * Suc (i + i)) (lessThan n) =
-    n * (# 4 * n * n - Numeral1)"
+  "3 * setsum (\<lambda>i. Suc (i + i) * Suc (i + i)) (lessThan n) =
+    n * (4 * n * n - Numeral1)"
   apply (induct n)
   txt {* This removes the @{term "-Numeral1"} from the inductive step *}
    apply (case_tac [2] n)
@@ -51,7 +51,7 @@
 
 lemma sum_of_odd_cubes:
   "setsum (\<lambda>i. Suc (i + i) * Suc (i + i) * Suc (i + i)) (lessThan n) =
-    n * n * (# 2 * n * n - Numeral1)"
+    n * n * (2 * n * n - Numeral1)"
   apply (induct "n")
   txt {* This removes the @{term "-Numeral1"} from the inductive step *}
    apply (case_tac [2] "n")
@@ -63,19 +63,19 @@
   @{text "n (n + 1) / 2"}.*}
 
 lemma sum_of_naturals:
-    "# 2 * setsum id (atMost n) = n * Suc n"
+    "2 * setsum id (atMost n) = n * Suc n"
   apply (induct n)
    apply auto
   done
 
 lemma sum_of_squares:
-    "# 6 * setsum (\<lambda>i. i * i) (atMost n) = n * Suc n * Suc (# 2 * n)"
+    "6 * setsum (\<lambda>i. i * i) (atMost n) = n * Suc n * Suc (2 * n)"
   apply (induct n)
    apply auto
   done
 
 lemma sum_of_cubes:
-    "# 4 * setsum (\<lambda>i. i * i * i) (atMost n) = n * n * Suc n * Suc n"
+    "4 * setsum (\<lambda>i. i * i * i) (atMost n) = n * n * Suc n * Suc n"
   apply (induct n)
    apply auto
   done
@@ -86,8 +86,8 @@
 *}
 
 lemma sum_of_fourth_powers:
-  "# 30 * setsum (\<lambda>i. i * i * i * i) (atMost n) =
-    n * Suc n * Suc (# 2 * n) * (# 3 * n * n + # 3 * n - Numeral1)"
+  "30 * setsum (\<lambda>i. i * i * i * i) (atMost n) =
+    n * Suc n * Suc (2 * n) * (3 * n * n + 3 * n - Numeral1)"
   apply (induct n)
    apply auto
   txt {* Eliminates the subtraction *}
@@ -107,9 +107,9 @@
   zdiff_zmult_distrib2 [simp]
 
 lemma int_sum_of_fourth_powers:
-  "# 30 * int (setsum (\<lambda>i. i * i * i * i) (lessThan m)) =
-    int m * (int m - Numeral1) * (int (# 2 * m) - Numeral1) *
-    (int (# 3 * m * m) - int (# 3 * m) - Numeral1)"
+  "30 * int (setsum (\<lambda>i. i * i * i * i) (lessThan m)) =
+    int m * (int m - Numeral1) * (int (2 * m) - Numeral1) *
+    (int (3 * m * m) - int (3 * m) - Numeral1)"
   apply (induct m)
    apply simp_all
   done
@@ -118,12 +118,12 @@
 text {*
   \medskip Sums of geometric series: 2, 3 and the general case *}
 
-lemma sum_of_2_powers: "setsum (\<lambda>i. # 2^i) (lessThan n) = # 2^n - (1::nat)"
+lemma sum_of_2_powers: "setsum (\<lambda>i. 2^i) (lessThan n) = 2^n - (1::nat)"
   apply (induct n)
    apply (auto split: nat_diff_split) 
   done
 
-lemma sum_of_3_powers: "# 2 * setsum (\<lambda>i. # 3^i) (lessThan n) = # 3^n - (1::nat)"
+lemma sum_of_3_powers: "2 * setsum (\<lambda>i. 3^i) (lessThan n) = 3^n - (1::nat)"
   apply (induct n)
    apply auto
   done
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/ex/Primrec.thy
--- a/src/HOL/ex/Primrec.thy	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/ex/Primrec.thy	Sat Oct 06 00:02:46 2001 +0200
@@ -159,7 +159,7 @@
 
 text {* PROPERTY A 8 *}
 
-lemma ack_1 [simp]: "ack (Suc 0, j) = j + # 2"
+lemma ack_1 [simp]: "ack (Suc 0, j) = j + 2"
   apply (induct j)
    apply simp_all
   done
@@ -168,7 +168,7 @@
 text {* PROPERTY A 9.  The unary @{text 1} and @{text 2} in @{term
   ack} is essential for the rewriting. *}
 
-lemma ack_2 [simp]: "ack (Suc (Suc 0), j) = # 2 * j + # 3"
+lemma ack_2 [simp]: "ack (Suc (Suc 0), j) = 2 * j + 3"
   apply (induct j)
    apply simp_all
   done
@@ -203,7 +203,7 @@
 
 text {* PROPERTY A 10 *}
 
-lemma ack_nest_bound: "ack(i1, ack (i2, j)) < ack (# 2 + (i1 + i2), j)"
+lemma ack_nest_bound: "ack(i1, ack (i2, j)) < ack (2 + (i1 + i2), j)"
   apply (simp add: numerals)
   apply (rule ack2_le_ack1 [THEN [2] less_le_trans])
   apply simp
@@ -215,7 +215,7 @@
 
 text {* PROPERTY A 11 *}
 
-lemma ack_add_bound: "ack (i1, j) + ack (i2, j) < ack (# 4 + (i1 + i2), j)"
+lemma ack_add_bound: "ack (i1, j) + ack (i2, j) < ack (4 + (i1 + i2), j)"
   apply (rule_tac j = "ack (Suc (Suc 0), ack (i1 + i2, j))" in less_trans)
    prefer 2
    apply (rule ack_nest_bound [THEN less_le_trans])
@@ -231,7 +231,7 @@
   used @{text "k + 4"}.  Quantified version must be nested @{text
   "\<exists>k'. \<forall>i j. ..."} *}
 
-lemma ack_add_bound2: "i < ack (k, j) ==> i + j < ack (# 4 + k, j)"
+lemma ack_add_bound2: "i < ack (k, j) ==> i + j < ack (4 + k, j)"
   apply (rule_tac j = "ack (k, j) + ack (0, j)" in less_trans)
    prefer 2
    apply (rule ack_add_bound [THEN less_le_trans])
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/ex/Records.thy
--- a/src/HOL/ex/Records.thy	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/ex/Records.thy	Sat Oct 06 00:02:46 2001 +0200
@@ -182,7 +182,7 @@
 
 constdefs
   foo10 :: nat
-  "foo10 == getX (| x = # 2, y = 0, colour = Blue |)"
+  "foo10 == getX (| x = 2, y = 0, colour = Blue |)"
 
 
 subsubsection {* Non-coercive structural subtyping *}
@@ -194,7 +194,7 @@
 
 constdefs
   foo11 :: cpoint
-  "foo11 == setX (| x = # 2, y = 0, colour = Blue |) 0"
+  "foo11 == setX (| x = 2, y = 0, colour = Blue |) 0"
 
 
 subsection {* Other features *}
@@ -207,7 +207,7 @@
 
 text {*
  \noindent May not apply @{term getX} to 
- @{term [source] "(| x' = # 2, y' = 0 |)"}.
+ @{term [source] "(| x' = 2, y' = 0 |)"}.
 *}
 
 text {* \medskip Polymorphic records. *}
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/ex/svc_test.ML
--- a/src/HOL/ex/svc_test.ML	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/ex/svc_test.ML	Sat Oct 06 00:02:46 2001 +0200
@@ -231,9 +231,9 @@
 
 (** Linear arithmetic **)
 
-Goal "x ~= # 14 & x ~= # 13 & x ~= # 12 & x ~= # 11 & x ~= # 10 & x ~= # 9 & \
-\     x ~= # 8 & x ~= # 7 & x ~= # 6 & x ~= # 5 & x ~= # 4 & x ~= # 3 & \
-\     x ~= # 2 & x ~= Numeral1 & Numeral0 < x & x < # 16 --> # 15 = (x::int)";
+Goal "x ~= 14 & x ~= 13 & x ~= 12 & x ~= 11 & x ~= 10 & x ~= 9 & \
+\     x ~= 8 & x ~= 7 & x ~= 6 & x ~= 5 & x ~= 4 & x ~= 3 & \
+\     x ~= 2 & x ~= Numeral1 & Numeral0 < x & x < 16 --> 15 = (x::int)";
 by (svc_tac 1);
 qed "";
 
@@ -244,11 +244,11 @@
 
 (** Natural number examples requiring implicit "non-negative" assumptions*)
 
-Goal "(# 3::nat)*a <= # 2 + # 4*b + # 6*c  & # 11 <= # 2*a + b + # 2*c & \
-\     a + # 3*b <= # 5 + # 2*c  --> # 2 + # 3*b <= # 2*a + # 6*c";
+Goal "(3::nat)*a <= 2 + 4*b + 6*c  & 11 <= 2*a + b + 2*c & \
+\     a + 3*b <= 5 + 2*c  --> 2 + 3*b <= 2*a + 6*c";
 by (svc_tac 1);
 qed "";
 
-Goal "(n::nat) < # 2 ==> (n = Numeral0) | (n = Numeral1)";
+Goal "(n::nat) < 2 ==> (n = Numeral0) | (n = Numeral1)";
 by (svc_tac 1);
 qed "";
diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOLCF/FOCUS/Buffer_adm.ML
--- a/src/HOLCF/FOCUS/Buffer_adm.ML	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOLCF/FOCUS/Buffer_adm.ML	Sat Oct 06 00:02:46 2001 +0200
@@ -110,7 +110,7 @@
 Goal "f:BufEq ==> ? l. !i x s. s:BufAC_Asm --> x << s --> Fin (l i) < #x --> \
 		\    (x,f\\<cdot>x):down_iterate BufAC_Cmt_F i --> \
 		\    (s,f\\<cdot>s):down_iterate BufAC_Cmt_F i";
-by (res_inst_tac [("x","%i. # 2*i")] exI 1);
+by (res_inst_tac [("x","%i. 2*i")] exI 1);
 by (rtac allI 1);
 by (nat_ind_tac "i" 1);
 by ( Simp_tac 1);
@@ -129,10 +129,10 @@
        \\<lbrakk>f \\<in> BufEq;
           \\<forall>x s. s \\<in> BufAC_Asm \\<longrightarrow>
                 x \\<sqsubseteq> s \\<longrightarrow>
-                Fin (# 2 * i) < #x \\<longrightarrow>
+                Fin (2 * i) < #x \\<longrightarrow>
                 (x, f\\<cdot>x) \\<in> down_iterate BufAC_Cmt_F i \\<longrightarrow>
                 (s, f\\<cdot>s) \\<in> down_iterate BufAC_Cmt_F i;
-          Md d\\<leadsto>\\<bullet>\\<leadsto>xa \\<in> BufAC_Asm; Fin (# 2 * i) < #ya; f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>ya) = d\\<leadsto>t;
+          Md d\\<leadsto>\\<bullet>\\<leadsto>xa \\<in> BufAC_Asm; Fin (2 * i) < #ya; f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>ya) = d\\<leadsto>t;
           (ya, t) \\<in> down_iterate BufAC_Cmt_F i; ya \\<sqsubseteq> xa\\<rbrakk>
        \\<Longrightarrow> (xa, rt\\<cdot>(f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>xa))) \\<in> down_iterate BufAC_Cmt_F i
 *)
@@ -147,11 +147,11 @@
 by (hyp_subst_tac 1);
 (*
  1. \\<And>i d xa ya t ff ffa.
-       \\<lbrakk>f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>ya) = d\\<leadsto>ffa\\<cdot>ya; Fin (# 2 * i) < #ya;
+       \\<lbrakk>f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>ya) = d\\<leadsto>ffa\\<cdot>ya; Fin (2 * i) < #ya;
           (ya, ffa\\<cdot>ya) \\<in> down_iterate BufAC_Cmt_F i; ya \\<sqsubseteq> xa; f \\<in> BufEq;
           \\<forall>x s. s \\<in> BufAC_Asm \\<longrightarrow>
                 x \\<sqsubseteq> s \\<longrightarrow>
-                Fin (# 2 * i) < #x \\<longrightarrow>
+                Fin (2 * i) < #x \\<longrightarrow>
                 (x, f\\<cdot>x) \\<in> down_iterate BufAC_Cmt_F i \\<longrightarrow>
                 (s, f\\<cdot>s) \\<in> down_iterate BufAC_Cmt_F i;
           xa \\<in> BufAC_Asm; ff \\<in> BufEq; ffa \\<in> BufEq\\<rbrakk>