* sane numerals (stage 2): plain "num" syntax (removed "#");
authorwenzelm
Sat Oct 06 00:02:46 2001 +0200 (2001-10-06)
changeset 117043c50a2cd6f00
parent 11703 6e5de8d4290a
child 11705 ac8ca15c556c
* sane numerals (stage 2): plain "num" syntax (removed "#");
src/HOL/Algebra/poly/PolyHomo.ML
src/HOL/Auth/KerberosIV.thy
src/HOL/Auth/Kerberos_BAN.thy
src/HOL/GroupTheory/Exponent.ML
src/HOL/Hoare/Arith2.ML
src/HOL/Hoare/Examples.ML
src/HOL/Hyperreal/HyperArith0.ML
src/HOL/Hyperreal/HyperBin.ML
src/HOL/Hyperreal/HyperPow.ML
src/HOL/Hyperreal/Lim.ML
src/HOL/Hyperreal/Lim.thy
src/HOL/Hyperreal/NSA.ML
src/HOL/Hyperreal/Series.ML
src/HOL/Hyperreal/hypreal_arith0.ML
src/HOL/IMP/Compiler.thy
src/HOL/IMP/Examples.ML
src/HOL/IMPP/EvenOdd.ML
src/HOL/IMPP/EvenOdd.thy
src/HOL/Induct/Mutil.thy
src/HOL/Integ/Bin.ML
src/HOL/Integ/IntArith.ML
src/HOL/Integ/IntDiv.ML
src/HOL/Integ/IntDiv.thy
src/HOL/Integ/NatSimprocs.ML
src/HOL/Integ/int_arith1.ML
src/HOL/Integ/int_arith2.ML
src/HOL/Integ/int_factor_simprocs.ML
src/HOL/Integ/nat_bin.ML
src/HOL/Integ/nat_simprocs.ML
src/HOL/Isar_examples/Fibonacci.thy
src/HOL/Isar_examples/HoareEx.thy
src/HOL/Isar_examples/MutilatedCheckerboard.thy
src/HOL/Isar_examples/Summation.thy
src/HOL/Lambda/Type.thy
src/HOL/Library/While_Combinator.thy
src/HOL/NumberTheory/EulerFermat.thy
src/HOL/NumberTheory/Fib.thy
src/HOL/NumberTheory/WilsonBij.thy
src/HOL/NumberTheory/WilsonRuss.thy
src/HOL/Numeral.thy
src/HOL/Real/HahnBanach/VectorSpace.thy
src/HOL/Real/RComplete.ML
src/HOL/Real/RealArith0.ML
src/HOL/Real/RealBin.ML
src/HOL/Real/RealPow.ML
src/HOL/Real/ex/BinEx.thy
src/HOL/Real/ex/Sqrt_Irrational.thy
src/HOL/Real/real_arith0.ML
src/HOL/UNITY/Simple/Mutex.ML
src/HOL/UNITY/Simple/Mutex.thy
src/HOL/UNITY/Union.ML
src/HOL/Unix/ROOT.ML
src/HOL/arith_data.ML
src/HOL/ex/BinEx.thy
src/HOL/ex/NatSum.thy
src/HOL/ex/Primrec.thy
src/HOL/ex/Records.thy
src/HOL/ex/svc_test.ML
src/HOLCF/FOCUS/Buffer_adm.ML
     1.1 --- a/src/HOL/Algebra/poly/PolyHomo.ML	Fri Oct 05 23:58:52 2001 +0200
     1.2 +++ b/src/HOL/Algebra/poly/PolyHomo.ML	Sat Oct 06 00:02:46 2001 +0200
     1.3 @@ -112,15 +112,15 @@
     1.4  (* Examples *)
     1.5  
     1.6  Goal
     1.7 -  "EVAL (x::'a::domain) (a*X^# 2 + b*X^1 + c*X^0) = a * x ^ # 2 + b * x ^ 1 + c";
     1.8 +  "EVAL (x::'a::domain) (a*X^2 + b*X^1 + c*X^0) = a * x ^ 2 + b * x ^ 1 + c";
     1.9  by (asm_simp_tac (simpset() delsimps [power_Suc]
    1.10      addsimps [EVAL_homo, EVAL_monom, EVAL_smult]) 1);
    1.11  result();
    1.12  
    1.13  Goal
    1.14    "EVAL (y::'a::domain) \
    1.15 -\    (EVAL (const x) (monom 1 + const (a*X^# 2 + b*X^1 + c*X^0))) = \
    1.16 -\  x ^ 1 + (a * y ^ # 2 + b * y ^ 1 + c)";
    1.17 +\    (EVAL (const x) (monom 1 + const (a*X^2 + b*X^1 + c*X^0))) = \
    1.18 +\  x ^ 1 + (a * y ^ 2 + b * y ^ 1 + c)";
    1.19  by (asm_simp_tac (simpset() delsimps [power_Suc]
    1.20      addsimps [EVAL_homo, EVAL_monom, EVAL_smult, EVAL_const]) 1);
    1.21  result();
     2.1 --- a/src/HOL/Auth/KerberosIV.thy	Fri Oct 05 23:58:52 2001 +0200
     2.2 +++ b/src/HOL/Auth/KerberosIV.thy	Sat Oct 06 00:02:46 2001 +0200
     2.3 @@ -65,8 +65,8 @@
     2.4      RespLife   :: nat 
     2.5  
     2.6  rules
     2.7 -     AuthLife_LB    "# 2 <= AuthLife"
     2.8 -     ServLife_LB    "# 2 <= ServLife"
     2.9 +     AuthLife_LB    "2 <= AuthLife"
    2.10 +     ServLife_LB    "2 <= ServLife"
    2.11       AutcLife_LB    "Suc 0 <= AutcLife" 
    2.12       RespLife_LB    "Suc 0 <= RespLife"
    2.13  
     3.1 --- a/src/HOL/Auth/Kerberos_BAN.thy	Fri Oct 05 23:58:52 2001 +0200
     3.2 +++ b/src/HOL/Auth/Kerberos_BAN.thy	Sat Oct 06 00:02:46 2001 +0200
     3.3 @@ -30,7 +30,7 @@
     3.4  
     3.5  rules
     3.6      (*The ticket should remain fresh for two journeys on the network at least*)
     3.7 -    SesKeyLife_LB "# 2 <= SesKeyLife"
     3.8 +    SesKeyLife_LB "2 <= SesKeyLife"
     3.9  
    3.10      (*The authenticator only for one journey*)
    3.11      AutLife_LB    "Suc 0 <= AutLife"
     4.1 --- a/src/HOL/GroupTheory/Exponent.ML	Fri Oct 05 23:58:52 2001 +0200
     4.2 +++ b/src/HOL/GroupTheory/Exponent.ML	Sat Oct 06 00:02:46 2001 +0200
     4.3 @@ -205,13 +205,13 @@
     4.4  by (induct_tac "n" 1);
     4.5  by (Asm_simp_tac 1); 
     4.6  by (Asm_full_simp_tac 1); 
     4.7 -by (subgoal_tac "# 2 * n + # 2 <= p * p^n" 1);
     4.8 +by (subgoal_tac "2 * n + 2 <= p * p^n" 1);
     4.9  by (Asm_full_simp_tac 1); 
    4.10 -by (subgoal_tac "# 2 * p^n <= p * p^n" 1);
    4.11 +by (subgoal_tac "2 * p^n <= p * p^n" 1);
    4.12  (*?arith_tac should handle all of this!*)
    4.13  by (rtac order_trans 1); 
    4.14  by (assume_tac 2); 
    4.15 -by (dres_inst_tac [("k","# 2")] mult_le_mono2 1); 
    4.16 +by (dres_inst_tac [("k","2")] mult_le_mono2 1); 
    4.17  by (Asm_full_simp_tac 1); 
    4.18  by (rtac mult_le_mono1 1); 
    4.19  by (Asm_full_simp_tac 1); 
     5.1 --- a/src/HOL/Hoare/Arith2.ML	Fri Oct 05 23:58:52 2001 +0200
     5.2 +++ b/src/HOL/Hoare/Arith2.ML	Sat Oct 06 00:02:46 2001 +0200
     5.3 @@ -63,7 +63,7 @@
     5.4  
     5.5  (*** pow ***)
     5.6  
     5.7 -Goal "m mod # 2 = 0 ==> ((n::nat)*n)^(m div # 2) = n^m";
     5.8 +Goal "m mod 2 = 0 ==> ((n::nat)*n)^(m div 2) = n^m";
     5.9  by (asm_simp_tac (simpset() addsimps [power_two RS sym, power_mult RS sym,
    5.10  				      mult_div_cancel]) 1);
    5.11  qed "sq_pow_div2";
     6.1 --- a/src/HOL/Hoare/Examples.ML	Fri Oct 05 23:58:52 2001 +0200
     6.2 +++ b/src/HOL/Hoare/Examples.ML	Sat Oct 06 00:02:46 2001 +0200
     6.3 @@ -50,9 +50,9 @@
     6.4  Goal "|- VARS a b x y. \
     6.5  \ {0<A & 0<B & a=A & b=B & x=B & y=A} \
     6.6  \ WHILE  a ~= b  \
     6.7 -\ INV {0<a & 0<b & gcd A B = gcd a b & # 2*A*B = a*x + b*y} \
     6.8 +\ INV {0<a & 0<b & gcd A B = gcd a b & 2*A*B = a*x + b*y} \
     6.9  \ DO IF a<b THEN (b := b-a; x := x+y) ELSE (a := a-b; y := y+x) FI OD \
    6.10 -\ {a = gcd A B & # 2*A*B = a*(x+y)}";
    6.11 +\ {a = gcd A B & 2*A*B = a*(x+y)}";
    6.12  by (hoare_tac (K all_tac) 1);
    6.13  by(Asm_simp_tac 1);
    6.14  by(asm_simp_tac (simpset() addsimps
    6.15 @@ -68,9 +68,9 @@
    6.16  \ c := (1::nat); \
    6.17  \ WHILE b ~= 0 \
    6.18  \ INV {A^B = c * a^b} \
    6.19 -\ DO  WHILE b mod # 2 = 0 \
    6.20 +\ DO  WHILE b mod 2 = 0 \
    6.21  \     INV {A^B = c * a^b} \
    6.22 -\     DO  a := a*a; b := b div # 2 OD; \
    6.23 +\     DO  a := a*a; b := b div 2 OD; \
    6.24  \     c := c*a; b := b - 1 \
    6.25  \ OD \
    6.26  \ {c = A^B}";
    6.27 @@ -114,7 +114,7 @@
    6.28  \ x := X; u := 1; w := 1; r := (0::nat); \
    6.29  \ WHILE w <= x \
    6.30  \ INV {u = r+r+1 & w = (r+1)*(r+1) & r*r <= x & x=X} \
    6.31 -\ DO r := r + 1; w := w + u + # 2; u := u + # 2 OD \
    6.32 +\ DO r := r + 1; w := w + u + 2; u := u + 2 OD \
    6.33  \ {r*r <= X & X < (r+1)*(r+1)}";
    6.34  by (hoare_tac (SELECT_GOAL Auto_tac) 1);
    6.35  qed "sqrt_without_multiplication";
     7.1 --- a/src/HOL/Hyperreal/HyperArith0.ML	Fri Oct 05 23:58:52 2001 +0200
     7.2 +++ b/src/HOL/Hyperreal/HyperArith0.ML	Sat Oct 06 00:02:46 2001 +0200
     7.3 @@ -288,34 +288,34 @@
     7.4  set trace_simp;
     7.5  fun test s = (Goal s; by (Simp_tac 1)); 
     7.6  
     7.7 -test "Numeral0 <= (y::hypreal) * # -2";
     7.8 -test "# 9*x = # 12 * (y::hypreal)";
     7.9 -test "(# 9*x) / (# 12 * (y::hypreal)) = z";
    7.10 -test "# 9*x < # 12 * (y::hypreal)";
    7.11 -test "# 9*x <= # 12 * (y::hypreal)";
    7.12 +test "Numeral0 <= (y::hypreal) * -2";
    7.13 +test "9*x = 12 * (y::hypreal)";
    7.14 +test "(9*x) / (12 * (y::hypreal)) = z";
    7.15 +test "9*x < 12 * (y::hypreal)";
    7.16 +test "9*x <= 12 * (y::hypreal)";
    7.17  
    7.18 -test "# -99*x = # 123 * (y::hypreal)";
    7.19 -test "(# -99*x) / (# 123 * (y::hypreal)) = z";
    7.20 -test "# -99*x < # 123 * (y::hypreal)";
    7.21 -test "# -99*x <= # 123 * (y::hypreal)";
    7.22 +test "-99*x = 123 * (y::hypreal)";
    7.23 +test "(-99*x) / (123 * (y::hypreal)) = z";
    7.24 +test "-99*x < 123 * (y::hypreal)";
    7.25 +test "-99*x <= 123 * (y::hypreal)";
    7.26  
    7.27 -test "# 999*x = # -396 * (y::hypreal)";
    7.28 -test "(# 999*x) / (# -396 * (y::hypreal)) = z";
    7.29 -test "# 999*x < # -396 * (y::hypreal)";
    7.30 -test "# 999*x <= # -396 * (y::hypreal)";
    7.31 +test "999*x = -396 * (y::hypreal)";
    7.32 +test "(999*x) / (-396 * (y::hypreal)) = z";
    7.33 +test "999*x < -396 * (y::hypreal)";
    7.34 +test "999*x <= -396 * (y::hypreal)";
    7.35  
    7.36 -test "# -99*x = # -81 * (y::hypreal)";
    7.37 -test "(# -99*x) / (# -81 * (y::hypreal)) = z";
    7.38 -test "# -99*x <= # -81 * (y::hypreal)";
    7.39 -test "# -99*x < # -81 * (y::hypreal)";
    7.40 +test "-99*x = -81 * (y::hypreal)";
    7.41 +test "(-99*x) / (-81 * (y::hypreal)) = z";
    7.42 +test "-99*x <= -81 * (y::hypreal)";
    7.43 +test "-99*x < -81 * (y::hypreal)";
    7.44  
    7.45 -test "# -2 * x = # -1 * (y::hypreal)";
    7.46 -test "# -2 * x = -(y::hypreal)";
    7.47 -test "(# -2 * x) / (# -1 * (y::hypreal)) = z";
    7.48 -test "# -2 * x < -(y::hypreal)";
    7.49 -test "# -2 * x <= # -1 * (y::hypreal)";
    7.50 -test "-x < # -23 * (y::hypreal)";
    7.51 -test "-x <= # -23 * (y::hypreal)";
    7.52 +test "-2 * x = -1 * (y::hypreal)";
    7.53 +test "-2 * x = -(y::hypreal)";
    7.54 +test "(-2 * x) / (-1 * (y::hypreal)) = z";
    7.55 +test "-2 * x < -(y::hypreal)";
    7.56 +test "-2 * x <= -1 * (y::hypreal)";
    7.57 +test "-x < -23 * (y::hypreal)";
    7.58 +test "-x <= -23 * (y::hypreal)";
    7.59  *)
    7.60  
    7.61  
    7.62 @@ -516,18 +516,18 @@
    7.63  qed "hypreal_divide_1";
    7.64  Addsimps [hypreal_divide_1];
    7.65  
    7.66 -Goal "x/# -1 = -(x::hypreal)";
    7.67 +Goal "x/-1 = -(x::hypreal)";
    7.68  by (Simp_tac 1); 
    7.69  qed "hypreal_divide_minus1";
    7.70  Addsimps [hypreal_divide_minus1];
    7.71  
    7.72 -Goal "# -1/(x::hypreal) = - (Numeral1/x)";
    7.73 +Goal "-1/(x::hypreal) = - (Numeral1/x)";
    7.74  by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_minus_inverse]) 1); 
    7.75  qed "hypreal_minus1_divide";
    7.76  Addsimps [hypreal_minus1_divide];
    7.77  
    7.78  Goal "[| (Numeral0::hypreal) < d1; Numeral0 < d2 |] ==> EX e. Numeral0 < e & e < d1 & e < d2";
    7.79 -by (res_inst_tac [("x","(min d1 d2)/# 2")] exI 1); 
    7.80 +by (res_inst_tac [("x","(min d1 d2)/2")] exI 1); 
    7.81  by (asm_simp_tac (simpset() addsimps [min_def]) 1); 
    7.82  qed "hypreal_lbound_gt_zero";
    7.83  
    7.84 @@ -644,11 +644,11 @@
    7.85  
    7.86  (*** Density of the Hyperreals ***)
    7.87  
    7.88 -Goal "x < y ==> x < (x+y) / (# 2::hypreal)";
    7.89 +Goal "x < y ==> x < (x+y) / (2::hypreal)";
    7.90  by Auto_tac;
    7.91  qed "hypreal_less_half_sum";
    7.92  
    7.93 -Goal "x < y ==> (x+y)/(# 2::hypreal) < y";
    7.94 +Goal "x < y ==> (x+y)/(2::hypreal) < y";
    7.95  by Auto_tac;
    7.96  qed "hypreal_gt_half_sum";
    7.97  
     8.1 --- a/src/HOL/Hyperreal/HyperBin.ML	Fri Oct 05 23:58:52 2001 +0200
     8.2 +++ b/src/HOL/Hyperreal/HyperBin.ML	Sat Oct 06 00:02:46 2001 +0200
     8.3 @@ -57,18 +57,18 @@
     8.4  qed "mult_hypreal_number_of";
     8.5  Addsimps [mult_hypreal_number_of];
     8.6  
     8.7 -Goal "(# 2::hypreal) = Numeral1 + Numeral1";
     8.8 +Goal "(2::hypreal) = Numeral1 + Numeral1";
     8.9  by (Simp_tac 1);
    8.10  val lemma = result();
    8.11  
    8.12  (*For specialist use: NOT as default simprules*)
    8.13 -Goal "# 2 * z = (z+z::hypreal)";
    8.14 +Goal "2 * z = (z+z::hypreal)";
    8.15  by (simp_tac (simpset ()
    8.16  	      addsimps [lemma, hypreal_add_mult_distrib,
    8.17  			one_eq_numeral_1 RS sym]) 1);
    8.18  qed "hypreal_mult_2";
    8.19  
    8.20 -Goal "z * # 2 = (z+z::hypreal)";
    8.21 +Goal "z * 2 = (z+z::hypreal)";
    8.22  by (stac hypreal_mult_commute 1 THEN rtac hypreal_mult_2 1);
    8.23  qed "hypreal_mult_2_right";
    8.24  
    8.25 @@ -107,11 +107,11 @@
    8.26  
    8.27  (*** New versions of existing theorems involving 0, 1hr ***)
    8.28  
    8.29 -Goal "- Numeral1 = (# -1::hypreal)";
    8.30 +Goal "- Numeral1 = (-1::hypreal)";
    8.31  by (Simp_tac 1);
    8.32  qed "minus_numeral_one";
    8.33  
    8.34 -(*Maps 0 to Numeral0 and 1hr to Numeral1 and -1hr to # -1*)
    8.35 +(*Maps 0 to Numeral0 and 1hr to Numeral1 and -1hr to -1*)
    8.36  val hypreal_numeral_ss = 
    8.37      real_numeral_ss addsimps [zero_eq_numeral_0, one_eq_numeral_1, 
    8.38  		              minus_numeral_one];
    8.39 @@ -242,14 +242,14 @@
    8.40                          hypreal_add_ac@rel_iff_rel_0_rls) 1);
    8.41  qed "hypreal_le_add_iff2";
    8.42  
    8.43 -Goal "(z::hypreal) * # -1 = -z";
    8.44 +Goal "(z::hypreal) * -1 = -z";
    8.45  by (stac (minus_numeral_one RS sym) 1);
    8.46  by (stac (hypreal_minus_mult_eq2 RS sym) 1); 
    8.47  by Auto_tac;  
    8.48  qed "hypreal_mult_minus_1_right";
    8.49  Addsimps [hypreal_mult_minus_1_right];
    8.50  
    8.51 -Goal "# -1 * (z::hypreal) = -z";
    8.52 +Goal "-1 * (z::hypreal) = -z";
    8.53  by (simp_tac (simpset() addsimps [hypreal_mult_commute]) 1); 
    8.54  qed "hypreal_mult_minus_1";
    8.55  Addsimps [hypreal_mult_minus_1];
    8.56 @@ -471,7 +471,7 @@
    8.57  structure CombineNumeralsData =
    8.58    struct
    8.59    val add		= op + : int*int -> int 
    8.60 -  val mk_sum    	= long_mk_sum    (*to work for e.g. # 2*x + # 3*x *)
    8.61 +  val mk_sum    	= long_mk_sum    (*to work for e.g. 2*x + 3*x *)
    8.62    val dest_sum		= dest_sum
    8.63    val mk_coeff		= mk_coeff
    8.64    val dest_coeff	= dest_coeff 1
    8.65 @@ -530,34 +530,34 @@
    8.66  set trace_simp;
    8.67  fun test s = (Goal s, by (Simp_tac 1)); 
    8.68  
    8.69 -test "l + # 2 + # 2 + # 2 + (l + # 2) + (oo + # 2) = (uu::hypreal)";
    8.70 -test "# 2*u = (u::hypreal)";
    8.71 -test "(i + j + # 12 + (k::hypreal)) - # 15 = y";
    8.72 -test "(i + j + # 12 + (k::hypreal)) - # 5 = y";
    8.73 +test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::hypreal)";
    8.74 +test "2*u = (u::hypreal)";
    8.75 +test "(i + j + 12 + (k::hypreal)) - 15 = y";
    8.76 +test "(i + j + 12 + (k::hypreal)) - 5 = y";
    8.77  
    8.78  test "y - b < (b::hypreal)";
    8.79 -test "y - (# 3*b + c) < (b::hypreal) - # 2*c";
    8.80 +test "y - (3*b + c) < (b::hypreal) - 2*c";
    8.81  
    8.82 -test "(# 2*x - (u*v) + y) - v*# 3*u = (w::hypreal)";
    8.83 -test "(# 2*x*u*v + (u*v)*# 4 + y) - v*u*# 4 = (w::hypreal)";
    8.84 -test "(# 2*x*u*v + (u*v)*# 4 + y) - v*u = (w::hypreal)";
    8.85 -test "u*v - (x*u*v + (u*v)*# 4 + y) = (w::hypreal)";
    8.86 +test "(2*x - (u*v) + y) - v*3*u = (w::hypreal)";
    8.87 +test "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::hypreal)";
    8.88 +test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::hypreal)";
    8.89 +test "u*v - (x*u*v + (u*v)*4 + y) = (w::hypreal)";
    8.90  
    8.91 -test "(i + j + # 12 + (k::hypreal)) = u + # 15 + y";
    8.92 -test "(i + j*# 2 + # 12 + (k::hypreal)) = j + # 5 + y";
    8.93 +test "(i + j + 12 + (k::hypreal)) = u + 15 + y";
    8.94 +test "(i + j*2 + 12 + (k::hypreal)) = j + 5 + y";
    8.95  
    8.96 -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)";
    8.97 +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)";
    8.98  
    8.99  test "a + -(b+c) + b = (d::hypreal)";
   8.100  test "a + -(b+c) - b = (d::hypreal)";
   8.101  
   8.102  (*negative numerals*)
   8.103 -test "(i + j + # -2 + (k::hypreal)) - (u + # 5 + y) = zz";
   8.104 -test "(i + j + # -3 + (k::hypreal)) < u + # 5 + y";
   8.105 -test "(i + j + # 3 + (k::hypreal)) < u + # -6 + y";
   8.106 -test "(i + j + # -12 + (k::hypreal)) - # 15 = y";
   8.107 -test "(i + j + # 12 + (k::hypreal)) - # -15 = y";
   8.108 -test "(i + j + # -12 + (k::hypreal)) - # -15 = y";
   8.109 +test "(i + j + -2 + (k::hypreal)) - (u + 5 + y) = zz";
   8.110 +test "(i + j + -3 + (k::hypreal)) < u + 5 + y";
   8.111 +test "(i + j + 3 + (k::hypreal)) < u + -6 + y";
   8.112 +test "(i + j + -12 + (k::hypreal)) - 15 = y";
   8.113 +test "(i + j + 12 + (k::hypreal)) - -15 = y";
   8.114 +test "(i + j + -12 + (k::hypreal)) - -15 = y";
   8.115  *)
   8.116  
   8.117  
     9.1 --- a/src/HOL/Hyperreal/HyperPow.ML	Fri Oct 05 23:58:52 2001 +0200
     9.2 +++ b/src/HOL/Hyperreal/HyperPow.ML	Sat Oct 06 00:02:46 2001 +0200
     9.3 @@ -75,7 +75,7 @@
     9.4  qed "hrabs_minus_hrealpow_one";
     9.5  Addsimps [hrabs_minus_hrealpow_one];
     9.6  
     9.7 -Goal "abs(# -1 ^ n) = (Numeral1::hypreal)";
     9.8 +Goal "abs(-1 ^ n) = (Numeral1::hypreal)";
     9.9  by (induct_tac "n" 1);
    9.10  by Auto_tac;  
    9.11  qed "hrabs_hrealpow_minus_one";
    9.12 @@ -134,13 +134,13 @@
    9.13  by Auto_tac;  
    9.14  qed "hrealpow_two_ge_one";
    9.15  
    9.16 -Goal "(Numeral1::hypreal) <= # 2 ^ n";
    9.17 +Goal "(Numeral1::hypreal) <= 2 ^ n";
    9.18  by (res_inst_tac [("y","Numeral1 ^ n")] order_trans 1);
    9.19  by (rtac hrealpow_le 2);
    9.20  by Auto_tac;
    9.21  qed "two_hrealpow_ge_one";
    9.22  
    9.23 -Goal "hypreal_of_nat n < # 2 ^ n";
    9.24 +Goal "hypreal_of_nat n < 2 ^ n";
    9.25  by (induct_tac "n" 1);
    9.26  by (auto_tac (claset(),
    9.27          simpset() addsimps [hypreal_of_nat_Suc, hypreal_add_mult_distrib]));
    9.28 @@ -149,17 +149,17 @@
    9.29  qed "two_hrealpow_gt";
    9.30  Addsimps [two_hrealpow_gt,two_hrealpow_ge_one];
    9.31  
    9.32 -Goal "# -1 ^ (# 2*n) = (Numeral1::hypreal)";
    9.33 +Goal "-1 ^ (2*n) = (Numeral1::hypreal)";
    9.34  by (induct_tac "n" 1);
    9.35  by (Auto_tac);
    9.36  qed "hrealpow_minus_one";
    9.37  
    9.38 -Goal "n+n = (# 2*n::nat)";
    9.39 +Goal "n+n = (2*n::nat)";
    9.40  by Auto_tac; 
    9.41  qed "double_lemma";
    9.42  
    9.43  (*ugh: need to get rid fo the n+n*)
    9.44 -Goal "# -1 ^ (n + n) = (Numeral1::hypreal)";
    9.45 +Goal "-1 ^ (n + n) = (Numeral1::hypreal)";
    9.46  by (auto_tac (claset(), 
    9.47                simpset() addsimps [double_lemma, hrealpow_minus_one]));
    9.48  qed "hrealpow_minus_one2";
    9.49 @@ -340,7 +340,7 @@
    9.50  qed "hrabs_minus_hyperpow_one";
    9.51  Addsimps [hrabs_minus_hyperpow_one];
    9.52  
    9.53 -Goal "abs(# -1 pow n) = (Numeral1::hypreal)";
    9.54 +Goal "abs(-1 pow n) = (Numeral1::hypreal)";
    9.55  by (subgoal_tac "abs((- 1hr) pow n) = 1hr" 1);
    9.56  by (Asm_full_simp_tac 1); 
    9.57  by (simp_tac (HOL_ss addsimps [hypreal_one_def]) 1);
    9.58 @@ -388,7 +388,7 @@
    9.59                simpset()));
    9.60  qed "hyperpow_two_ge_one";
    9.61  
    9.62 -Goal "(Numeral1::hypreal) <= # 2 pow n";
    9.63 +Goal "(Numeral1::hypreal) <= 2 pow n";
    9.64  by (res_inst_tac [("y","Numeral1 pow n")] order_trans 1);
    9.65  by (rtac hyperpow_le 2);
    9.66  by Auto_tac;
    9.67 @@ -397,7 +397,7 @@
    9.68  
    9.69  Addsimps [simplify (simpset()) realpow_minus_one];
    9.70  
    9.71 -Goal "# -1 pow ((1hn + 1hn)*n) = (Numeral1::hypreal)";
    9.72 +Goal "-1 pow ((1hn + 1hn)*n) = (Numeral1::hypreal)";
    9.73  by (subgoal_tac "(-(1hr)) pow ((1hn + 1hn)*n) = 1hr" 1);
    9.74  by (Asm_full_simp_tac 1); 
    9.75  by (simp_tac (HOL_ss addsimps [hypreal_one_def]) 1);
    10.1 --- a/src/HOL/Hyperreal/Lim.ML	Fri Oct 05 23:58:52 2001 +0200
    10.2 +++ b/src/HOL/Hyperreal/Lim.ML	Sat Oct 06 00:02:46 2001 +0200
    10.3 @@ -29,7 +29,7 @@
    10.4  Goalw [LIM_def] 
    10.5       "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + g(x)) -- x --> (l + m)";
    10.6  by (Clarify_tac 1);
    10.7 -by (REPEAT(dres_inst_tac [("x","r/# 2")] spec 1));
    10.8 +by (REPEAT(dres_inst_tac [("x","r/2")] spec 1));
    10.9  by (Asm_full_simp_tac 1);
   10.10  by (Clarify_tac 1);
   10.11  by (res_inst_tac [("R1.0","s"),("R2.0","sa")] 
   10.12 @@ -1544,15 +1544,15 @@
   10.13                simpset() addsimps [Bolzano_bisect_le, Let_def, split_def]));  
   10.14  qed "Bolzano_bisect_Suc_le_snd";
   10.15  
   10.16 -Goal "((x::real) = y / (# 2 * z)) = (# 2 * x = y/z)";
   10.17 +Goal "((x::real) = y / (2 * z)) = (2 * x = y/z)";
   10.18  by Auto_tac;  
   10.19 -by (dres_inst_tac [("f","%u. (Numeral1/# 2)*u")] arg_cong 1); 
   10.20 +by (dres_inst_tac [("f","%u. (Numeral1/2)*u")] arg_cong 1); 
   10.21  by Auto_tac;  
   10.22  qed "eq_divide_2_times_iff";
   10.23  
   10.24  Goal "a \\<le> b ==> \
   10.25  \     snd(Bolzano_bisect P a b n) - fst(Bolzano_bisect P a b n) = \
   10.26 -\     (b-a) / (# 2 ^ n)";
   10.27 +\     (b-a) / (2 ^ n)";
   10.28  by (induct_tac "n" 1);
   10.29  by (auto_tac (claset(), 
   10.30        simpset() addsimps [eq_divide_2_times_iff, real_add_divide_distrib, 
   10.31 @@ -1604,8 +1604,8 @@
   10.32  by (rename_tac "l" 1);
   10.33  by (dres_inst_tac [("x","l")] spec 1 THEN Clarify_tac 1);
   10.34  by (rewtac LIMSEQ_def);
   10.35 -by (dres_inst_tac [("P", "%r. Numeral0<r --> ?Q r"), ("x","d/# 2")] spec 1);
   10.36 -by (dres_inst_tac [("P", "%r. Numeral0<r --> ?Q r"), ("x","d/# 2")] spec 1);
   10.37 +by (dres_inst_tac [("P", "%r. Numeral0<r --> ?Q r"), ("x","d/2")] spec 1);
   10.38 +by (dres_inst_tac [("P", "%r. Numeral0<r --> ?Q r"), ("x","d/2")] spec 1);
   10.39  by (dtac real_less_half_sum 1);
   10.40  by Safe_tac;
   10.41  (*linear arithmetic bug if we just use Asm_simp_tac*)
   10.42 @@ -2148,12 +2148,12 @@
   10.43                simpset() addsimps [real_mult_assoc]));
   10.44  qed "DERIV_const_ratio_const2";
   10.45  
   10.46 -Goal "((a + b) /# 2 - a) = (b - a)/(# 2::real)";
   10.47 +Goal "((a + b) /2 - a) = (b - a)/(2::real)";
   10.48  by Auto_tac;  
   10.49  qed "real_average_minus_first";
   10.50  Addsimps [real_average_minus_first];
   10.51  
   10.52 -Goal "((b + a)/# 2 - a) = (b - a)/(# 2::real)";
   10.53 +Goal "((b + a)/2 - a) = (b - a)/(2::real)";
   10.54  by Auto_tac;  
   10.55  qed "real_average_minus_second";
   10.56  Addsimps [real_average_minus_second];
   10.57 @@ -2161,7 +2161,7 @@
   10.58  
   10.59  (* Gallileo's "trick": average velocity = av. of end velocities *)
   10.60  Goal "[|a \\<noteq> (b::real); \\<forall>x. DERIV v x :> k|] \
   10.61 -\     ==> v((a + b)/# 2) = (v a + v b)/# 2";
   10.62 +\     ==> v((a + b)/2) = (v a + v b)/2";
   10.63  by (res_inst_tac [("R1.0","a"),("R2.0","b")] real_linear_less2 1);
   10.64  by Auto_tac;
   10.65  by (ftac DERIV_const_ratio_const2 1 THEN assume_tac 1);
    11.1 --- a/src/HOL/Hyperreal/Lim.thy	Fri Oct 05 23:58:52 2001 +0200
    11.2 +++ b/src/HOL/Hyperreal/Lim.thy	Sat Oct 06 00:02:46 2001 +0200
    11.3 @@ -71,8 +71,8 @@
    11.4    "Bolzano_bisect P a b 0 = (a,b)"
    11.5    "Bolzano_bisect P a b (Suc n) =
    11.6        (let (x,y) = Bolzano_bisect P a b n
    11.7 -       in if P(x, (x+y)/# 2) then ((x+y)/# 2, y)
    11.8 -                            else (x, (x+y)/# 2) )"
    11.9 +       in if P(x, (x+y)/2) then ((x+y)/2, y)
   11.10 +                            else (x, (x+y)/2) )"
   11.11    
   11.12  
   11.13  end
    12.1 --- a/src/HOL/Hyperreal/NSA.ML	Fri Oct 05 23:58:52 2001 +0200
    12.2 +++ b/src/HOL/Hyperreal/NSA.ML	Sat Oct 06 00:02:46 2001 +0200
    12.3 @@ -260,11 +260,11 @@
    12.4  qed "Infinitesimal_zero";
    12.5  AddIffs [Infinitesimal_zero];
    12.6  
    12.7 -Goal "x/(# 2::hypreal) + x/(# 2::hypreal) = x";
    12.8 +Goal "x/(2::hypreal) + x/(2::hypreal) = x";
    12.9  by Auto_tac;  
   12.10  qed "hypreal_sum_of_halves";
   12.11  
   12.12 -Goal "Numeral0 < r ==> Numeral0 < r/(# 2::hypreal)";
   12.13 +Goal "Numeral0 < r ==> Numeral0 < r/(2::hypreal)";
   12.14  by Auto_tac;  
   12.15  qed "hypreal_half_gt_zero";
   12.16  
    13.1 --- a/src/HOL/Hyperreal/Series.ML	Fri Oct 05 23:58:52 2001 +0200
    13.2 +++ b/src/HOL/Hyperreal/Series.ML	Sat Oct 06 00:02:46 2001 +0200
    13.3 @@ -101,7 +101,7 @@
    13.4  by (Auto_tac);
    13.5  qed "sumr_shift_bounds";
    13.6  
    13.7 -Goal "sumr 0 (# 2*n) (%i. (# -1) ^ Suc i) = Numeral0";
    13.8 +Goal "sumr 0 (2*n) (%i. (-1) ^ Suc i) = Numeral0";
    13.9  by (induct_tac "n" 1);
   13.10  by (Auto_tac);
   13.11  qed "sumr_minus_one_realpow_zero";
    14.1 --- a/src/HOL/Hyperreal/hypreal_arith0.ML	Fri Oct 05 23:58:52 2001 +0200
    14.2 +++ b/src/HOL/Hyperreal/hypreal_arith0.ML	Sat Oct 06 00:02:46 2001 +0200
    14.3 @@ -115,7 +115,7 @@
    14.4  qed "";
    14.5  
    14.6  Goal "!!a::hypreal. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
    14.7 -\     ==> # 6*a <= # 5*l+i";
    14.8 +\     ==> 6*a <= 5*l+i";
    14.9  by (fast_arith_tac 1);
   14.10  qed "";
   14.11  *)
    15.1 --- a/src/HOL/IMP/Compiler.thy	Fri Oct 05 23:58:52 2001 +0200
    15.2 +++ b/src/HOL/IMP/Compiler.thy	Sat Oct 06 00:02:46 2001 +0200
    15.3 @@ -39,9 +39,9 @@
    15.4  "compile (x:==a) = [ASIN x a]"
    15.5  "compile (c1;c2) = compile c1 @ compile c2"
    15.6  "compile (IF b THEN c1 ELSE c2) =
    15.7 - [JMPF b (length(compile c1) + # 2)] @ compile c1 @
    15.8 + [JMPF b (length(compile c1) + 2)] @ compile c1 @
    15.9   [JMPF (%x. False) (length(compile c2)+1)] @ compile c2"
   15.10 -"compile (WHILE b DO c) = [JMPF b (length(compile c) + # 2)] @ compile c @
   15.11 +"compile (WHILE b DO c) = [JMPF b (length(compile c) + 2)] @ compile c @
   15.12   [JMPB (length(compile c)+1)]"
   15.13  
   15.14  declare nth_append[simp];
    16.1 --- a/src/HOL/IMP/Examples.ML	Fri Oct 05 23:58:52 2001 +0200
    16.2 +++ b/src/HOL/IMP/Examples.ML	Sat Oct 06 00:02:46 2001 +0200
    16.3 @@ -34,7 +34,7 @@
    16.4  val step = resolve_tac evalc.intrs 1;
    16.5  val simp = Asm_simp_tac 1;
    16.6  Goalw [factorial_def] "a~=b ==> \
    16.7 -\ <factorial a b, Mem(a:=# 3)>  -c-> Mem(b:=# 6,a:=Numeral0)";
    16.8 +\ <factorial a b, Mem(a:=3)>  -c-> Mem(b:=6,a:=Numeral0)";
    16.9  by (ftac not_sym 1);
   16.10  by step;
   16.11  by  step;
    17.1 --- a/src/HOL/IMPP/EvenOdd.ML	Fri Oct 05 23:58:52 2001 +0200
    17.2 +++ b/src/HOL/IMPP/EvenOdd.ML	Sat Oct 06 00:02:46 2001 +0200
    17.3 @@ -17,7 +17,7 @@
    17.4  Addsimps [not_even_1];
    17.5  
    17.6  Goalw [even_def] "even (Suc (Suc n)) = even n";
    17.7 -by (subgoal_tac "Suc (Suc n) = n+# 2" 1);
    17.8 +by (subgoal_tac "Suc (Suc n) = n+2" 1);
    17.9  by  (Simp_tac 2);
   17.10  by (etac ssubst 1);
   17.11  by (rtac dvd_reduce 1);
    18.1 --- a/src/HOL/IMPP/EvenOdd.thy	Fri Oct 05 23:58:52 2001 +0200
    18.2 +++ b/src/HOL/IMPP/EvenOdd.thy	Sat Oct 06 00:02:46 2001 +0200
    18.3 @@ -9,7 +9,7 @@
    18.4  EvenOdd = Misc +
    18.5  
    18.6  constdefs even :: nat => bool
    18.7 -  "even n == # 2 dvd n"
    18.8 +  "even n == 2 dvd n"
    18.9  
   18.10  consts
   18.11    Even, Odd :: pname
    19.1 --- a/src/HOL/Induct/Mutil.thy	Fri Oct 05 23:58:52 2001 +0200
    19.2 +++ b/src/HOL/Induct/Mutil.thy	Sat Oct 06 00:02:46 2001 +0200
    19.3 @@ -29,7 +29,7 @@
    19.4  
    19.5  constdefs
    19.6    coloured :: "nat => (nat \<times> nat) set"
    19.7 -   "coloured b == {(i, j). (i + j) mod # 2 = b}"
    19.8 +   "coloured b == {(i, j). (i + j) mod 2 = b}"
    19.9  
   19.10  
   19.11  text {* \medskip The union of two disjoint tilings is a tiling *}
   19.12 @@ -61,14 +61,14 @@
   19.13    apply auto
   19.14    done
   19.15  
   19.16 -lemma dominoes_tile_row [intro!]: "{i} \<times> lessThan (# 2 * n) \<in> tiling domino"
   19.17 +lemma dominoes_tile_row [intro!]: "{i} \<times> lessThan (2 * n) \<in> tiling domino"
   19.18    apply (induct n)
   19.19     apply (simp_all add: Un_assoc [symmetric])
   19.20    apply (rule tiling.Un)
   19.21      apply (auto simp add: sing_Times_lemma)
   19.22    done
   19.23  
   19.24 -lemma dominoes_tile_matrix: "(lessThan m) \<times> lessThan (# 2 * n) \<in> tiling domino"
   19.25 +lemma dominoes_tile_matrix: "(lessThan m) \<times> lessThan (2 * n) \<in> tiling domino"
   19.26    apply (induct m)
   19.27     apply auto
   19.28    done
   19.29 @@ -78,7 +78,7 @@
   19.30  
   19.31  lemma coloured_insert [simp]:
   19.32    "coloured b \<inter> (insert (i, j) t) =
   19.33 -   (if (i + j) mod # 2 = b then insert (i, j) (coloured b \<inter> t)
   19.34 +   (if (i + j) mod 2 = b then insert (i, j) (coloured b \<inter> t)
   19.35      else coloured b \<inter> t)"
   19.36    apply (unfold coloured_def)
   19.37    apply auto
   19.38 @@ -125,7 +125,7 @@
   19.39  
   19.40  theorem gen_mutil_not_tiling:
   19.41    "t \<in> tiling domino ==>
   19.42 -    (i + j) mod # 2 = 0 ==> (m + n) mod # 2 = 0 ==>
   19.43 +    (i + j) mod 2 = 0 ==> (m + n) mod 2 = 0 ==>
   19.44      {(i, j), (m, n)} \<subseteq> t
   19.45    ==> (t - {(i, j)} - {(m, n)}) \<notin> tiling domino"
   19.46    apply (rule notI)
   19.47 @@ -140,8 +140,8 @@
   19.48  text {* Apply the general theorem to the well-known case *}
   19.49  
   19.50  theorem mutil_not_tiling:
   19.51 -  "t = lessThan (# 2 * Suc m) \<times> lessThan (# 2 * Suc n)
   19.52 -    ==> t - {(0, 0)} - {(Suc (# 2 * m), Suc (# 2 * n))} \<notin> tiling domino"
   19.53 +  "t = lessThan (2 * Suc m) \<times> lessThan (2 * Suc n)
   19.54 +    ==> t - {(0, 0)} - {(Suc (2 * m), Suc (2 * n))} \<notin> tiling domino"
   19.55    apply (rule gen_mutil_not_tiling)
   19.56       apply (blast intro!: dominoes_tile_matrix)
   19.57      apply auto
    20.1 --- a/src/HOL/Integ/Bin.ML	Fri Oct 05 23:58:52 2001 +0200
    20.2 +++ b/src/HOL/Integ/Bin.ML	Sat Oct 06 00:02:46 2001 +0200
    20.3 @@ -160,7 +160,7 @@
    20.4  
    20.5  (*The correctness of shifting.  But it doesn't seem to give a measurable
    20.6    speed-up.*)
    20.7 -Goal "(# 2::int) * number_of w = number_of (w BIT False)";
    20.8 +Goal "(2::int) * number_of w = number_of (w BIT False)";
    20.9  by (induct_tac "w" 1);
   20.10  by (ALLGOALS (asm_simp_tac
   20.11      (simpset() addsimps bin_mult_simps @ [zadd_zmult_distrib] @ zadd_ac)));
   20.12 @@ -250,11 +250,11 @@
   20.13  by (Simp_tac 1);
   20.14  qed "zmult_1_right";
   20.15  
   20.16 -Goal "# -1 * z = -(z::int)";
   20.17 +Goal "-1 * z = -(z::int)";
   20.18  by (simp_tac (simpset() addsimps zcompare_rls@[zmult_zminus]) 1);
   20.19  qed "zmult_minus1";
   20.20  
   20.21 -Goal "z * # -1 = -(z::int)";
   20.22 +Goal "z * -1 = -(z::int)";
   20.23  by (simp_tac (simpset() addsimps zcompare_rls@[zmult_zminus_right]) 1);
   20.24  qed "zmult_minus1_right";
   20.25  
    21.1 --- a/src/HOL/Integ/IntArith.ML	Fri Oct 05 23:58:52 2001 +0200
    21.2 +++ b/src/HOL/Integ/IntArith.ML	Sat Oct 06 00:02:46 2001 +0200
    21.3 @@ -168,7 +168,7 @@
    21.4  by Auto_tac;  
    21.5  qed "pos_zmult_eq_1_iff";
    21.6  
    21.7 -Goal "(m*n = (Numeral1::int)) = ((m = Numeral1 & n = Numeral1) | (m = # -1 & n = # -1))";
    21.8 +Goal "(m*n = (Numeral1::int)) = ((m = Numeral1 & n = Numeral1) | (m = -1 & n = -1))";
    21.9  by (case_tac "Numeral0<m" 1);
   21.10  by (asm_simp_tac (simpset() addsimps [pos_zmult_eq_1_iff]) 1);
   21.11  by (case_tac "m=Numeral0" 1);
    22.1 --- a/src/HOL/Integ/IntDiv.ML	Fri Oct 05 23:58:52 2001 +0200
    22.2 +++ b/src/HOL/Integ/IntDiv.ML	Sat Oct 06 00:02:46 2001 +0200
    22.3 @@ -84,8 +84,8 @@
    22.4  
    22.5  
    22.6  Goal "adjust a b (q,r) = (let diff = r-b in \
    22.7 -\                         if Numeral0 <= diff then (# 2*q + Numeral1, diff)  \
    22.8 -\                                       else (# 2*q, r))";
    22.9 +\                         if Numeral0 <= diff then (2*q + Numeral1, diff)  \
   22.10 +\                                       else (2*q, r))";
   22.11  by (simp_tac (simpset() addsimps [Let_def,adjust_def]) 1);
   22.12  qed "adjust_eq";
   22.13  Addsimps [adjust_eq];
   22.14 @@ -103,7 +103,7 @@
   22.15  (**use with simproc to avoid re-proving the premise*)
   22.16  Goal "Numeral0 < b ==> \
   22.17  \     posDivAlg (a,b) =      \
   22.18 -\      (if a<b then (Numeral0,a) else adjust a b (posDivAlg(a, # 2*b)))";
   22.19 +\      (if a<b then (Numeral0,a) else adjust a b (posDivAlg(a, 2*b)))";
   22.20  by (rtac (posDivAlg_raw_eqn RS trans) 1);
   22.21  by (Asm_simp_tac 1);
   22.22  qed "posDivAlg_eqn";
   22.23 @@ -141,7 +141,7 @@
   22.24  (**use with simproc to avoid re-proving the premise*)
   22.25  Goal "Numeral0 < b ==> \
   22.26  \     negDivAlg (a,b) =      \
   22.27 -\      (if Numeral0<=a+b then (# -1,a+b) else adjust a b (negDivAlg(a, # 2*b)))";
   22.28 +\      (if Numeral0<=a+b then (-1,a+b) else adjust a b (negDivAlg(a, 2*b)))";
   22.29  by (rtac (negDivAlg_raw_eqn RS trans) 1);
   22.30  by (Asm_simp_tac 1);
   22.31  qed "negDivAlg_eqn";
   22.32 @@ -179,7 +179,7 @@
   22.33  qed "posDivAlg_0";
   22.34  Addsimps [posDivAlg_0];
   22.35  
   22.36 -Goal "negDivAlg (# -1, b) = (# -1, b-Numeral1)";
   22.37 +Goal "negDivAlg (-1, b) = (-1, b-Numeral1)";
   22.38  by (stac negDivAlg_raw_eqn 1);
   22.39  by Auto_tac;
   22.40  qed "negDivAlg_minus1";
   22.41 @@ -272,7 +272,7 @@
   22.42  by (auto_tac (claset(), simpset() addsimps [quorem_def]));
   22.43  qed "div_neg_neg_trivial";
   22.44  
   22.45 -Goal "[| (Numeral0::int) < a;  a+b <= Numeral0 |] ==> a div b = # -1";
   22.46 +Goal "[| (Numeral0::int) < a;  a+b <= Numeral0 |] ==> a div b = -1";
   22.47  by (rtac quorem_div 1);
   22.48  by (auto_tac (claset(), simpset() addsimps [quorem_def]));
   22.49  qed "div_pos_neg_trivial";
   22.50 @@ -290,7 +290,7 @@
   22.51  qed "mod_neg_neg_trivial";
   22.52  
   22.53  Goal "[| (Numeral0::int) < a;  a+b <= Numeral0 |] ==> a mod b = a+b";
   22.54 -by (res_inst_tac [("q","# -1")] quorem_mod 1);
   22.55 +by (res_inst_tac [("q","-1")] quorem_mod 1);
   22.56  by (auto_tac (claset(), simpset() addsimps [quorem_def]));
   22.57  qed "mod_pos_neg_trivial";
   22.58  
   22.59 @@ -411,7 +411,7 @@
   22.60  by (simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
   22.61  qed "zdiv_zero";
   22.62  
   22.63 -Goal "(Numeral0::int) < b ==> # -1 div b = # -1";
   22.64 +Goal "(Numeral0::int) < b ==> -1 div b = -1";
   22.65  by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
   22.66  qed "div_eq_minus1";
   22.67  
   22.68 @@ -421,11 +421,11 @@
   22.69  
   22.70  Addsimps [zdiv_zero, zmod_zero];
   22.71  
   22.72 -Goal "(Numeral0::int) < b ==> # -1 div b = # -1";
   22.73 +Goal "(Numeral0::int) < b ==> -1 div b = -1";
   22.74  by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
   22.75  qed "zdiv_minus1";
   22.76  
   22.77 -Goal "(Numeral0::int) < b ==> # -1 mod b = b-Numeral1";
   22.78 +Goal "(Numeral0::int) < b ==> -1 mod b = b-Numeral1";
   22.79  by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
   22.80  qed "zmod_minus1";
   22.81  
   22.82 @@ -491,15 +491,15 @@
   22.83  qed "zdiv_1";
   22.84  Addsimps [zdiv_1];
   22.85  
   22.86 -Goal "a mod (# -1::int) = Numeral0";
   22.87 -by (cut_inst_tac [("a","a"),("b","# -1")] neg_mod_sign 1);
   22.88 -by (cut_inst_tac [("a","a"),("b","# -1")] neg_mod_bound 2);
   22.89 +Goal "a mod (-1::int) = Numeral0";
   22.90 +by (cut_inst_tac [("a","a"),("b","-1")] neg_mod_sign 1);
   22.91 +by (cut_inst_tac [("a","a"),("b","-1")] neg_mod_bound 2);
   22.92  by Auto_tac;
   22.93  qed "zmod_minus1_right";
   22.94  Addsimps [zmod_minus1_right];
   22.95  
   22.96 -Goal "a div (# -1::int) = -a";
   22.97 -by (cut_inst_tac [("a","a"),("b","# -1")] zmod_zdiv_equality 1);
   22.98 +Goal "a div (-1::int) = -a";
   22.99 +by (cut_inst_tac [("a","a"),("b","-1")] zmod_zdiv_equality 1);
  22.100  by Auto_tac;
  22.101  qed "zdiv_minus1_right";
  22.102  Addsimps [zdiv_minus1_right];
  22.103 @@ -861,13 +861,13 @@
  22.104  
  22.105  (** computing "div" by shifting **)
  22.106  
  22.107 -Goal "(Numeral0::int) <= a ==> (Numeral1 + # 2*b) div (# 2*a) = b div a";
  22.108 +Goal "(Numeral0::int) <= a ==> (Numeral1 + 2*b) div (2*a) = b div a";
  22.109  by (zdiv_undefined_case_tac "a = Numeral0" 1);
  22.110  by (subgoal_tac "Numeral1 <= a" 1);
  22.111   by (arith_tac 2);
  22.112 -by (subgoal_tac "Numeral1 < a * # 2" 1);
  22.113 +by (subgoal_tac "Numeral1 < a * 2" 1);
  22.114   by (arith_tac 2);
  22.115 -by (subgoal_tac "# 2*(Numeral1 + b mod a) <= # 2*a" 1);
  22.116 +by (subgoal_tac "2*(Numeral1 + b mod a) <= 2*a" 1);
  22.117   by (rtac zmult_zle_mono2 2);
  22.118  by (auto_tac (claset(),
  22.119  	      simpset() addsimps [zadd_commute, zmult_commute, 
  22.120 @@ -887,12 +887,12 @@
  22.121  qed "pos_zdiv_mult_2";
  22.122  
  22.123  
  22.124 -Goal "a <= (Numeral0::int) ==> (Numeral1 + # 2*b) div (# 2*a) = (b+Numeral1) div a";
  22.125 -by (subgoal_tac "(Numeral1 + # 2*(-b-Numeral1)) div (# 2 * (-a)) = (-b-Numeral1) div (-a)" 1);
  22.126 +Goal "a <= (Numeral0::int) ==> (Numeral1 + 2*b) div (2*a) = (b+Numeral1) div a";
  22.127 +by (subgoal_tac "(Numeral1 + 2*(-b-Numeral1)) div (2 * (-a)) = (-b-Numeral1) div (-a)" 1);
  22.128  by (rtac pos_zdiv_mult_2 2);
  22.129  by (auto_tac (claset(),
  22.130  	      simpset() addsimps [zmult_zminus_right]));
  22.131 -by (subgoal_tac "(# -1 - (# 2 * b)) = - (Numeral1 + (# 2 * b))" 1);
  22.132 +by (subgoal_tac "(-1 - (2 * b)) = - (Numeral1 + (2 * b))" 1);
  22.133  by (Simp_tac 2);
  22.134  by (asm_full_simp_tac (HOL_ss
  22.135  		       addsimps [zdiv_zminus_zminus, zdiff_def,
  22.136 @@ -921,13 +921,13 @@
  22.137  
  22.138  (** computing "mod" by shifting (proofs resemble those for "div") **)
  22.139  
  22.140 -Goal "(Numeral0::int) <= a ==> (Numeral1 + # 2*b) mod (# 2*a) = Numeral1 + # 2 * (b mod a)";
  22.141 +Goal "(Numeral0::int) <= a ==> (Numeral1 + 2*b) mod (2*a) = Numeral1 + 2 * (b mod a)";
  22.142  by (zdiv_undefined_case_tac "a = Numeral0" 1);
  22.143  by (subgoal_tac "Numeral1 <= a" 1);
  22.144   by (arith_tac 2);
  22.145 -by (subgoal_tac "Numeral1 < a * # 2" 1);
  22.146 +by (subgoal_tac "Numeral1 < a * 2" 1);
  22.147   by (arith_tac 2);
  22.148 -by (subgoal_tac "# 2*(Numeral1 + b mod a) <= # 2*a" 1);
  22.149 +by (subgoal_tac "2*(Numeral1 + b mod a) <= 2*a" 1);
  22.150   by (rtac zmult_zle_mono2 2);
  22.151  by (auto_tac (claset(),
  22.152  	      simpset() addsimps [zadd_commute, zmult_commute, 
  22.153 @@ -947,13 +947,13 @@
  22.154  qed "pos_zmod_mult_2";
  22.155  
  22.156  
  22.157 -Goal "a <= (Numeral0::int) ==> (Numeral1 + # 2*b) mod (# 2*a) = # 2 * ((b+Numeral1) mod a) - Numeral1";
  22.158 +Goal "a <= (Numeral0::int) ==> (Numeral1 + 2*b) mod (2*a) = 2 * ((b+Numeral1) mod a) - Numeral1";
  22.159  by (subgoal_tac 
  22.160 -    "(Numeral1 + # 2*(-b-Numeral1)) mod (# 2*(-a)) = Numeral1 + # 2*((-b-Numeral1) mod (-a))" 1);
  22.161 +    "(Numeral1 + 2*(-b-Numeral1)) mod (2*(-a)) = Numeral1 + 2*((-b-Numeral1) mod (-a))" 1);
  22.162  by (rtac pos_zmod_mult_2 2);
  22.163  by (auto_tac (claset(),
  22.164  	      simpset() addsimps [zmult_zminus_right]));
  22.165 -by (subgoal_tac "(# -1 - (# 2 * b)) = - (Numeral1 + (# 2 * b))" 1);
  22.166 +by (subgoal_tac "(-1 - (2 * b)) = - (Numeral1 + (2 * b))" 1);
  22.167  by (Simp_tac 2);
  22.168  by (asm_full_simp_tac (HOL_ss
  22.169  		       addsimps [zmod_zminus_zminus, zdiff_def,
  22.170 @@ -965,9 +965,9 @@
  22.171  Goal "number_of (v BIT b) mod number_of (w BIT False) = \
  22.172  \         (if b then \
  22.173  \               if (Numeral0::int) <= number_of w \
  22.174 -\               then # 2 * (number_of v mod number_of w) + Numeral1    \
  22.175 -\               else # 2 * ((number_of v + (Numeral1::int)) mod number_of w) - Numeral1  \
  22.176 -\          else # 2 * (number_of v mod number_of w))";
  22.177 +\               then 2 * (number_of v mod number_of w) + Numeral1    \
  22.178 +\               else 2 * ((number_of v + (Numeral1::int)) mod number_of w) - Numeral1  \
  22.179 +\          else 2 * (number_of v mod number_of w))";
  22.180  by (simp_tac (simpset_of Int.thy addsimps [zadd_assoc, number_of_BIT]) 1);
  22.181  by (asm_simp_tac (simpset()
  22.182  		  delsimps bin_arith_extra_simps@bin_rel_simps
  22.183 @@ -981,10 +981,10 @@
  22.184  (** Quotients of signs **)
  22.185  
  22.186  Goal "[| a < (Numeral0::int);  Numeral0 < b |] ==> a div b < Numeral0";
  22.187 -by (subgoal_tac "a div b <= # -1" 1);
  22.188 +by (subgoal_tac "a div b <= -1" 1);
  22.189  by (Force_tac 1);
  22.190  by (rtac order_trans 1);
  22.191 -by (res_inst_tac [("a'","# -1")]  zdiv_mono1 1);
  22.192 +by (res_inst_tac [("a'","-1")]  zdiv_mono1 1);
  22.193  by (auto_tac (claset(), simpset() addsimps [zdiv_minus1]));
  22.194  qed "div_neg_pos_less0";
  22.195  
    23.1 --- a/src/HOL/Integ/IntDiv.thy	Fri Oct 05 23:58:52 2001 +0200
    23.2 +++ b/src/HOL/Integ/IntDiv.thy	Sat Oct 06 00:02:46 2001 +0200
    23.3 @@ -15,8 +15,8 @@
    23.4                        (if Numeral0 < b then Numeral0<=r & r<b else b<r & r <= Numeral0)"
    23.5  
    23.6    adjust :: "[int, int, int*int] => int*int"
    23.7 -    "adjust a b == %(q,r). if Numeral0 <= r-b then (# 2*q + Numeral1, r-b)
    23.8 -                           else (# 2*q, r)"
    23.9 +    "adjust a b == %(q,r). if Numeral0 <= r-b then (2*q + Numeral1, r-b)
   23.10 +                           else (2*q, r)"
   23.11  
   23.12  (** the division algorithm **)
   23.13  
   23.14 @@ -25,14 +25,14 @@
   23.15  recdef posDivAlg "inv_image less_than (%(a,b). nat(a - b + Numeral1))"
   23.16      "posDivAlg (a,b) =
   23.17         (if (a<b | b<=Numeral0) then (Numeral0,a)
   23.18 -        else adjust a b (posDivAlg(a, # 2*b)))"
   23.19 +        else adjust a b (posDivAlg(a, 2*b)))"
   23.20  
   23.21  (*for the case a<0, b>0*)
   23.22  consts negDivAlg :: "int*int => int*int"
   23.23  recdef negDivAlg "inv_image less_than (%(a,b). nat(- a - b))"
   23.24      "negDivAlg (a,b) =
   23.25 -       (if (Numeral0<=a+b | b<=Numeral0) then (# -1,a+b)
   23.26 -        else adjust a b (negDivAlg(a, # 2*b)))"
   23.27 +       (if (Numeral0<=a+b | b<=Numeral0) then (-1,a+b)
   23.28 +        else adjust a b (negDivAlg(a, 2*b)))"
   23.29  
   23.30  (*for the general case b~=0*)
   23.31  
    24.1 --- a/src/HOL/Integ/NatSimprocs.ML	Fri Oct 05 23:58:52 2001 +0200
    24.2 +++ b/src/HOL/Integ/NatSimprocs.ML	Sat Oct 06 00:02:46 2001 +0200
    24.3 @@ -92,40 +92,40 @@
    24.4  
    24.5  (** Evens and Odds, for Mutilated Chess Board **)
    24.6  
    24.7 -(*Case analysis on b<# 2*)
    24.8 -Goal "(n::nat) < # 2 ==> n = Numeral0 | n = Numeral1";
    24.9 +(*Case analysis on b<2*)
   24.10 +Goal "(n::nat) < 2 ==> n = Numeral0 | n = Numeral1";
   24.11  by (arith_tac 1);
   24.12  qed "less_2_cases";
   24.13  
   24.14 -Goal "Suc(Suc(m)) mod # 2 = m mod # 2";
   24.15 -by (subgoal_tac "m mod # 2 < # 2" 1);
   24.16 +Goal "Suc(Suc(m)) mod 2 = m mod 2";
   24.17 +by (subgoal_tac "m mod 2 < 2" 1);
   24.18  by (Asm_simp_tac 2);
   24.19  be (less_2_cases RS disjE) 1;
   24.20  by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_Suc])));
   24.21  qed "mod2_Suc_Suc";
   24.22  Addsimps [mod2_Suc_Suc];
   24.23  
   24.24 -Goal "!!m::nat. (0 < m mod # 2) = (m mod # 2 = Numeral1)";
   24.25 -by (subgoal_tac "m mod # 2 < # 2" 1);
   24.26 +Goal "!!m::nat. (0 < m mod 2) = (m mod 2 = Numeral1)";
   24.27 +by (subgoal_tac "m mod 2 < 2" 1);
   24.28  by (Asm_simp_tac 2);
   24.29  by (auto_tac (claset(), simpset() delsimps [mod_less_divisor]));
   24.30  qed "mod2_gr_0";
   24.31  Addsimps [mod2_gr_0, rename_numerals mod2_gr_0];
   24.32  
   24.33 -(** Removal of small numerals: Numeral0, Numeral1 and (in additive positions) # 2 **)
   24.34 +(** Removal of small numerals: Numeral0, Numeral1 and (in additive positions) 2 **)
   24.35  
   24.36 -Goal "# 2 + n = Suc (Suc n)";
   24.37 +Goal "2 + n = Suc (Suc n)";
   24.38  by (Simp_tac 1);
   24.39  qed "add_2_eq_Suc";
   24.40  
   24.41 -Goal "n + # 2 = Suc (Suc n)";
   24.42 +Goal "n + 2 = Suc (Suc n)";
   24.43  by (Simp_tac 1);
   24.44  qed "add_2_eq_Suc'";
   24.45  
   24.46  Addsimps [numeral_0_eq_0, numeral_1_eq_1, add_2_eq_Suc, add_2_eq_Suc'];
   24.47  
   24.48  (*Can be used to eliminate long strings of Sucs, but not by default*)
   24.49 -Goal "Suc (Suc (Suc n)) = # 3 + n";
   24.50 +Goal "Suc (Suc (Suc n)) = 3 + n";
   24.51  by (Simp_tac 1);
   24.52  qed "Suc3_eq_add_3";
   24.53  
   24.54 @@ -136,21 +136,21 @@
   24.55      We already have some rules to simplify operands smaller than 3.
   24.56  **)
   24.57  
   24.58 -Goal "m div (Suc (Suc (Suc n))) = m div (# 3+n)";
   24.59 +Goal "m div (Suc (Suc (Suc n))) = m div (3+n)";
   24.60  by (simp_tac (simpset() addsimps [Suc3_eq_add_3]) 1);
   24.61  qed "div_Suc_eq_div_add3";
   24.62  
   24.63 -Goal "m mod (Suc (Suc (Suc n))) = m mod (# 3+n)";
   24.64 +Goal "m mod (Suc (Suc (Suc n))) = m mod (3+n)";
   24.65  by (simp_tac (simpset() addsimps [Suc3_eq_add_3]) 1);
   24.66  qed "mod_Suc_eq_mod_add3";
   24.67  
   24.68  Addsimps [div_Suc_eq_div_add3, mod_Suc_eq_mod_add3];
   24.69  
   24.70 -Goal "(Suc (Suc (Suc m))) div n = (# 3+m) div n";
   24.71 +Goal "(Suc (Suc (Suc m))) div n = (3+m) div n";
   24.72  by (simp_tac (simpset() addsimps [Suc3_eq_add_3]) 1);
   24.73  qed "Suc_div_eq_add3_div";
   24.74  
   24.75 -Goal "(Suc (Suc (Suc m))) mod n = (# 3+m) mod n";
   24.76 +Goal "(Suc (Suc (Suc m))) mod n = (3+m) mod n";
   24.77  by (simp_tac (simpset() addsimps [Suc3_eq_add_3]) 1);
   24.78  qed "Suc_mod_eq_add3_mod";
   24.79  
    25.1 --- a/src/HOL/Integ/int_arith1.ML	Fri Oct 05 23:58:52 2001 +0200
    25.2 +++ b/src/HOL/Integ/int_arith1.ML	Sat Oct 06 00:02:46 2001 +0200
    25.3 @@ -279,7 +279,7 @@
    25.4  structure CombineNumeralsData =
    25.5    struct
    25.6    val add		= op + : int*int -> int 
    25.7 -  val mk_sum    	= long_mk_sum    (*to work for e.g. # 2*x + # 3*x *)
    25.8 +  val mk_sum    	= long_mk_sum    (*to work for e.g. 2*x + 3*x *)
    25.9    val dest_sum		= dest_sum
   25.10    val mk_coeff		= mk_coeff
   25.11    val dest_coeff	= dest_coeff 1
   25.12 @@ -318,35 +318,35 @@
   25.13  set trace_simp;
   25.14  fun test s = (Goal s; by (Simp_tac 1)); 
   25.15  
   25.16 -test "l + # 2 + # 2 + # 2 + (l + # 2) + (oo + # 2) = (uu::int)";
   25.17 +test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)";
   25.18  
   25.19 -test "# 2*u = (u::int)";
   25.20 -test "(i + j + # 12 + (k::int)) - # 15 = y";
   25.21 -test "(i + j + # 12 + (k::int)) - # 5 = y";
   25.22 +test "2*u = (u::int)";
   25.23 +test "(i + j + 12 + (k::int)) - 15 = y";
   25.24 +test "(i + j + 12 + (k::int)) - 5 = y";
   25.25  
   25.26  test "y - b < (b::int)";
   25.27 -test "y - (# 3*b + c) < (b::int) - # 2*c";
   25.28 +test "y - (3*b + c) < (b::int) - 2*c";
   25.29  
   25.30 -test "(# 2*x - (u*v) + y) - v*# 3*u = (w::int)";
   25.31 -test "(# 2*x*u*v + (u*v)*# 4 + y) - v*u*# 4 = (w::int)";
   25.32 -test "(# 2*x*u*v + (u*v)*# 4 + y) - v*u = (w::int)";
   25.33 -test "u*v - (x*u*v + (u*v)*# 4 + y) = (w::int)";
   25.34 +test "(2*x - (u*v) + y) - v*3*u = (w::int)";
   25.35 +test "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::int)";
   25.36 +test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::int)";
   25.37 +test "u*v - (x*u*v + (u*v)*4 + y) = (w::int)";
   25.38  
   25.39 -test "(i + j + # 12 + (k::int)) = u + # 15 + y";
   25.40 -test "(i + j*# 2 + # 12 + (k::int)) = j + # 5 + y";
   25.41 +test "(i + j + 12 + (k::int)) = u + 15 + y";
   25.42 +test "(i + j*2 + 12 + (k::int)) = j + 5 + y";
   25.43  
   25.44 -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)";
   25.45 +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)";
   25.46  
   25.47  test "a + -(b+c) + b = (d::int)";
   25.48  test "a + -(b+c) - b = (d::int)";
   25.49  
   25.50  (*negative numerals*)
   25.51 -test "(i + j + # -2 + (k::int)) - (u + # 5 + y) = zz";
   25.52 -test "(i + j + # -3 + (k::int)) < u + # 5 + y";
   25.53 -test "(i + j + # 3 + (k::int)) < u + # -6 + y";
   25.54 -test "(i + j + # -12 + (k::int)) - # 15 = y";
   25.55 -test "(i + j + # 12 + (k::int)) - # -15 = y";
   25.56 -test "(i + j + # -12 + (k::int)) - # -15 = y";
   25.57 +test "(i + j + -2 + (k::int)) - (u + 5 + y) = zz";
   25.58 +test "(i + j + -3 + (k::int)) < u + 5 + y";
   25.59 +test "(i + j + 3 + (k::int)) < u + -6 + y";
   25.60 +test "(i + j + -12 + (k::int)) - 15 = y";
   25.61 +test "(i + j + 12 + (k::int)) - -15 = y";
   25.62 +test "(i + j + -12 + (k::int)) - -15 = y";
   25.63  *)
   25.64  
   25.65  
   25.66 @@ -455,7 +455,7 @@
   25.67  (* Some test data
   25.68  Goal "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
   25.69  by (fast_arith_tac 1);
   25.70 -Goal "!!a::int. [| a < b; c < d |] ==> a-d+ # 2 <= b+(-c)";
   25.71 +Goal "!!a::int. [| a < b; c < d |] ==> a-d+ 2 <= b+(-c)";
   25.72  by (fast_arith_tac 1);
   25.73  Goal "!!a::int. [| a < b; c < d |] ==> a+c+ Numeral1 < b+d";
   25.74  by (fast_arith_tac 1);
   25.75 @@ -465,7 +465,7 @@
   25.76  \     ==> a+a <= j+j";
   25.77  by (fast_arith_tac 1);
   25.78  Goal "!!a::int. [| a+b < i+j; a<b; i<j |] \
   25.79 -\     ==> a+a - - # -1 < j+j - # 3";
   25.80 +\     ==> a+a - - -1 < j+j - 3";
   25.81  by (fast_arith_tac 1);
   25.82  Goal "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
   25.83  by (arith_tac 1);
   25.84 @@ -482,6 +482,6 @@
   25.85  \     ==> a+a+a+a+a+a <= l+l+l+l+i+l";
   25.86  by (fast_arith_tac 1);
   25.87  Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   25.88 -\     ==> # 6*a <= # 5*l+i";
   25.89 +\     ==> 6*a <= 5*l+i";
   25.90  by (fast_arith_tac 1);
   25.91  *)
    26.1 --- a/src/HOL/Integ/int_arith2.ML	Fri Oct 05 23:58:52 2001 +0200
    26.2 +++ b/src/HOL/Integ/int_arith2.ML	Sat Oct 06 00:02:46 2001 +0200
    26.3 @@ -75,7 +75,7 @@
    26.4  by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
    26.5  qed "nat_1";
    26.6  
    26.7 -Goal "nat # 2 = Suc (Suc 0)";
    26.8 +Goal "nat 2 = Suc (Suc 0)";
    26.9  by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
   26.10  qed "nat_2";
   26.11  
    27.1 --- a/src/HOL/Integ/int_factor_simprocs.ML	Fri Oct 05 23:58:52 2001 +0200
    27.2 +++ b/src/HOL/Integ/int_factor_simprocs.ML	Sat Oct 06 00:02:46 2001 +0200
    27.3 @@ -114,33 +114,33 @@
    27.4  set trace_simp;
    27.5  fun test s = (Goal s; by (Simp_tac 1)); 
    27.6  
    27.7 -test "# 9*x = # 12 * (y::int)";
    27.8 -test "(# 9*x) div (# 12 * (y::int)) = z";
    27.9 -test "# 9*x < # 12 * (y::int)";
   27.10 -test "# 9*x <= # 12 * (y::int)";
   27.11 +test "9*x = 12 * (y::int)";
   27.12 +test "(9*x) div (12 * (y::int)) = z";
   27.13 +test "9*x < 12 * (y::int)";
   27.14 +test "9*x <= 12 * (y::int)";
   27.15  
   27.16 -test "# -99*x = # 132 * (y::int)";
   27.17 -test "(# -99*x) div (# 132 * (y::int)) = z";
   27.18 -test "# -99*x < # 132 * (y::int)";
   27.19 -test "# -99*x <= # 132 * (y::int)";
   27.20 +test "-99*x = 132 * (y::int)";
   27.21 +test "(-99*x) div (132 * (y::int)) = z";
   27.22 +test "-99*x < 132 * (y::int)";
   27.23 +test "-99*x <= 132 * (y::int)";
   27.24  
   27.25 -test "# 999*x = # -396 * (y::int)";
   27.26 -test "(# 999*x) div (# -396 * (y::int)) = z";
   27.27 -test "# 999*x < # -396 * (y::int)";
   27.28 -test "# 999*x <= # -396 * (y::int)";
   27.29 +test "999*x = -396 * (y::int)";
   27.30 +test "(999*x) div (-396 * (y::int)) = z";
   27.31 +test "999*x < -396 * (y::int)";
   27.32 +test "999*x <= -396 * (y::int)";
   27.33  
   27.34 -test "# -99*x = # -81 * (y::int)";
   27.35 -test "(# -99*x) div (# -81 * (y::int)) = z";
   27.36 -test "# -99*x <= # -81 * (y::int)";
   27.37 -test "# -99*x < # -81 * (y::int)";
   27.38 +test "-99*x = -81 * (y::int)";
   27.39 +test "(-99*x) div (-81 * (y::int)) = z";
   27.40 +test "-99*x <= -81 * (y::int)";
   27.41 +test "-99*x < -81 * (y::int)";
   27.42  
   27.43 -test "# -2 * x = # -1 * (y::int)";
   27.44 -test "# -2 * x = -(y::int)";
   27.45 -test "(# -2 * x) div (# -1 * (y::int)) = z";
   27.46 -test "# -2 * x < -(y::int)";
   27.47 -test "# -2 * x <= # -1 * (y::int)";
   27.48 -test "-x < # -23 * (y::int)";
   27.49 -test "-x <= # -23 * (y::int)";
   27.50 +test "-2 * x = -1 * (y::int)";
   27.51 +test "-2 * x = -(y::int)";
   27.52 +test "(-2 * x) div (-1 * (y::int)) = z";
   27.53 +test "-2 * x < -(y::int)";
   27.54 +test "-2 * x <= -1 * (y::int)";
   27.55 +test "-x < -23 * (y::int)";
   27.56 +test "-x <= -23 * (y::int)";
   27.57  *)
   27.58  
   27.59  
    28.1 --- a/src/HOL/Integ/nat_bin.ML	Fri Oct 05 23:58:52 2001 +0200
    28.2 +++ b/src/HOL/Integ/nat_bin.ML	Sat Oct 06 00:02:46 2001 +0200
    28.3 @@ -25,7 +25,7 @@
    28.4  by (simp_tac (HOL_basic_ss addsimps [nat_1, nat_number_of_def, One_nat_def]) 1);
    28.5  qed "numeral_1_eq_1";
    28.6  
    28.7 -Goal "# 2 = Suc 1";
    28.8 +Goal "2 = Suc 1";
    28.9  by (simp_tac (HOL_basic_ss addsimps [nat_2, nat_number_of_def, One_nat_def]) 1);
   28.10  qed "numeral_2_eq_2";
   28.11  
   28.12 @@ -77,7 +77,7 @@
   28.13  by (Simp_tac 1);
   28.14  qed "Suc_numeral_0_eq_1";
   28.15  
   28.16 -Goal "Suc Numeral1 = # 2";
   28.17 +Goal "Suc Numeral1 = 2";
   28.18  by (Simp_tac 1);
   28.19  qed "Suc_numeral_1_eq_2";
   28.20  
   28.21 @@ -384,7 +384,7 @@
   28.22  qed "power_one";
   28.23  Addsimps [power_zero, power_one];
   28.24  
   28.25 -Goal "(p::nat) ^ # 2 = p*p";
   28.26 +Goal "(p::nat) ^ 2 = p*p";
   28.27  by (simp_tac numeral_ss 1);
   28.28  qed "power_two";
   28.29  
   28.30 @@ -497,7 +497,7 @@
   28.31  
   28.32  Goal "m+m ~= int (Suc 0) + n + n";
   28.33  by Auto_tac;
   28.34 -by (dres_inst_tac [("f", "%x. x mod # 2")] arg_cong 1);
   28.35 +by (dres_inst_tac [("f", "%x. x mod 2")] arg_cong 1);
   28.36  by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); 
   28.37  val lemma2 = result();
   28.38  
   28.39 @@ -514,7 +514,7 @@
   28.40  by (res_inst_tac [("x", "number_of v")] spec 1);
   28.41  by Safe_tac;
   28.42  by (ALLGOALS Full_simp_tac);
   28.43 -by (dres_inst_tac [("f", "%x. x mod # 2")] arg_cong 1);
   28.44 +by (dres_inst_tac [("f", "%x. x mod 2")] arg_cong 1);
   28.45  by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); 
   28.46  qed "eq_number_of_BIT_Pls"; 
   28.47  
   28.48 @@ -524,7 +524,7 @@
   28.49  	       [number_of_BIT, number_of_Min, eq_commute]) 1); 
   28.50  by (res_inst_tac [("x", "number_of v")] spec 1);
   28.51  by Auto_tac;
   28.52 -by (dres_inst_tac [("f", "%x. x mod # 2")] arg_cong 1);
   28.53 +by (dres_inst_tac [("f", "%x. x mod 2")] arg_cong 1);
   28.54  by Auto_tac;
   28.55  qed "eq_number_of_BIT_Min"; 
   28.56  
    29.1 --- a/src/HOL/Integ/nat_simprocs.ML	Fri Oct 05 23:58:52 2001 +0200
    29.2 +++ b/src/HOL/Integ/nat_simprocs.ML	Sat Oct 06 00:02:46 2001 +0200
    29.3 @@ -319,7 +319,7 @@
    29.4  structure CombineNumeralsData =
    29.5    struct
    29.6    val add		= op + : int*int -> int 
    29.7 -  val mk_sum            = long_mk_sum    (*to work for e.g. # 2*x + # 3*x *)
    29.8 +  val mk_sum            = long_mk_sum    (*to work for e.g. 2*x + 3*x *)
    29.9    val dest_sum          = restricted_dest_Sucs_sum
   29.10    val mk_coeff          = mk_coeff
   29.11    val dest_coeff        = dest_coeff
   29.12 @@ -504,62 +504,62 @@
   29.13  fun test s = (Goal s; by (Simp_tac 1));
   29.14  
   29.15  (*cancel_numerals*)
   29.16 -test "l +( # 2) + (# 2) + # 2 + (l + # 2) + (oo  + # 2) = (uu::nat)";
   29.17 -test "(# 2*length xs < # 2*length xs + j)";
   29.18 -test "(# 2*length xs < length xs * # 2 + j)";
   29.19 -test "# 2*u = (u::nat)";
   29.20 -test "# 2*u = Suc (u)";
   29.21 -test "(i + j + # 12 + (k::nat)) - # 15 = y";
   29.22 -test "(i + j + # 12 + (k::nat)) - # 5 = y";
   29.23 -test "Suc u - # 2 = y";
   29.24 -test "Suc (Suc (Suc u)) - # 2 = y";
   29.25 -test "(i + j + # 2 + (k::nat)) - 1 = y";
   29.26 +test "l +( 2) + (2) + 2 + (l + 2) + (oo  + 2) = (uu::nat)";
   29.27 +test "(2*length xs < 2*length xs + j)";
   29.28 +test "(2*length xs < length xs * 2 + j)";
   29.29 +test "2*u = (u::nat)";
   29.30 +test "2*u = Suc (u)";
   29.31 +test "(i + j + 12 + (k::nat)) - 15 = y";
   29.32 +test "(i + j + 12 + (k::nat)) - 5 = y";
   29.33 +test "Suc u - 2 = y";
   29.34 +test "Suc (Suc (Suc u)) - 2 = y";
   29.35 +test "(i + j + 2 + (k::nat)) - 1 = y";
   29.36  test "(i + j + Numeral1 + (k::nat)) - 2 = y";
   29.37  
   29.38 -test "(# 2*x + (u*v) + y) - v*# 3*u = (w::nat)";
   29.39 -test "(# 2*x*u*v + # 5 + (u*v)*# 4 + y) - v*u*# 4 = (w::nat)";
   29.40 -test "(# 2*x*u*v + (u*v)*# 4 + y) - v*u = (w::nat)";
   29.41 -test "Suc (Suc (# 2*x*u*v + u*# 4 + y)) - u = w";
   29.42 -test "Suc ((u*v)*# 4) - v*# 3*u = w";
   29.43 -test "Suc (Suc ((u*v)*# 3)) - v*# 3*u = w";
   29.44 +test "(2*x + (u*v) + y) - v*3*u = (w::nat)";
   29.45 +test "(2*x*u*v + 5 + (u*v)*4 + y) - v*u*4 = (w::nat)";
   29.46 +test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::nat)";
   29.47 +test "Suc (Suc (2*x*u*v + u*4 + y)) - u = w";
   29.48 +test "Suc ((u*v)*4) - v*3*u = w";
   29.49 +test "Suc (Suc ((u*v)*3)) - v*3*u = w";
   29.50  
   29.51 -test "(i + j + # 12 + (k::nat)) = u + # 15 + y";
   29.52 -test "(i + j + # 32 + (k::nat)) - (u + # 15 + y) = zz";
   29.53 -test "(i + j + # 12 + (k::nat)) = u + # 5 + y";
   29.54 +test "(i + j + 12 + (k::nat)) = u + 15 + y";
   29.55 +test "(i + j + 32 + (k::nat)) - (u + 15 + y) = zz";
   29.56 +test "(i + j + 12 + (k::nat)) = u + 5 + y";
   29.57  (*Suc*)
   29.58 -test "(i + j + # 12 + k) = Suc (u + y)";
   29.59 -test "Suc (Suc (Suc (Suc (Suc (u + y))))) <= ((i + j) + # 41 + k)";
   29.60 -test "(i + j + # 5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))";
   29.61 -test "Suc (Suc (Suc (Suc (Suc (u + y))))) - # 5 = v";
   29.62 -test "(i + j + # 5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))";
   29.63 -test "# 2*y + # 3*z + # 2*u = Suc (u)";
   29.64 -test "# 2*y + # 3*z + # 6*w + # 2*y + # 3*z + # 2*u = Suc (u)";
   29.65 -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)";
   29.66 -test "# 6 + # 2*y + # 3*z + # 4*u = Suc (vv + # 2*u + z)";
   29.67 -test "(# 2*n*m) < (# 3*(m*n)) + (u::nat)";
   29.68 +test "(i + j + 12 + k) = Suc (u + y)";
   29.69 +test "Suc (Suc (Suc (Suc (Suc (u + y))))) <= ((i + j) + 41 + k)";
   29.70 +test "(i + j + 5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))";
   29.71 +test "Suc (Suc (Suc (Suc (Suc (u + y))))) - 5 = v";
   29.72 +test "(i + j + 5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))";
   29.73 +test "2*y + 3*z + 2*u = Suc (u)";
   29.74 +test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = Suc (u)";
   29.75 +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)";
   29.76 +test "6 + 2*y + 3*z + 4*u = Suc (vv + 2*u + z)";
   29.77 +test "(2*n*m) < (3*(m*n)) + (u::nat)";
   29.78  
   29.79  (*negative numerals: FAIL*)
   29.80 -test "(i + j + # -23 + (k::nat)) < u + # 15 + y";
   29.81 -test "(i + j + # 3 + (k::nat)) < u + # -15 + y";
   29.82 -test "(i + j + # -12 + (k::nat)) - # 15 = y";
   29.83 -test "(i + j + # 12 + (k::nat)) - # -15 = y";
   29.84 -test "(i + j + # -12 + (k::nat)) - # -15 = y";
   29.85 +test "(i + j + -23 + (k::nat)) < u + 15 + y";
   29.86 +test "(i + j + 3 + (k::nat)) < u + -15 + y";
   29.87 +test "(i + j + -12 + (k::nat)) - 15 = y";
   29.88 +test "(i + j + 12 + (k::nat)) - -15 = y";
   29.89 +test "(i + j + -12 + (k::nat)) - -15 = y";
   29.90  
   29.91  (*combine_numerals*)
   29.92 -test "k + # 3*k = (u::nat)";
   29.93 -test "Suc (i + # 3) = u";
   29.94 -test "Suc (i + j + # 3 + k) = u";
   29.95 -test "k + j + # 3*k + j = (u::nat)";
   29.96 -test "Suc (j*i + i + k + # 5 + # 3*k + i*j*# 4) = (u::nat)";
   29.97 -test "(# 2*n*m) + (# 3*(m*n)) = (u::nat)";
   29.98 +test "k + 3*k = (u::nat)";
   29.99 +test "Suc (i + 3) = u";
  29.100 +test "Suc (i + j + 3 + k) = u";
  29.101 +test "k + j + 3*k + j = (u::nat)";
  29.102 +test "Suc (j*i + i + k + 5 + 3*k + i*j*4) = (u::nat)";
  29.103 +test "(2*n*m) + (3*(m*n)) = (u::nat)";
  29.104  (*negative numerals: FAIL*)
  29.105 -test "Suc (i + j + # -3 + k) = u";
  29.106 +test "Suc (i + j + -3 + k) = u";
  29.107  
  29.108  (*cancel_numeral_factors*)
  29.109 -test "# 9*x = # 12 * (y::nat)";
  29.110 -test "(# 9*x) div (# 12 * (y::nat)) = z";
  29.111 -test "# 9*x < # 12 * (y::nat)";
  29.112 -test "# 9*x <= # 12 * (y::nat)";
  29.113 +test "9*x = 12 * (y::nat)";
  29.114 +test "(9*x) div (12 * (y::nat)) = z";
  29.115 +test "9*x < 12 * (y::nat)";
  29.116 +test "9*x <= 12 * (y::nat)";
  29.117  
  29.118  (*cancel_factor*)
  29.119  test "x*k = k*(y::nat)";
    30.1 --- a/src/HOL/Isar_examples/Fibonacci.thy	Fri Oct 05 23:58:52 2001 +0200
    30.2 +++ b/src/HOL/Isar_examples/Fibonacci.thy	Sat Oct 06 00:02:46 2001 +0200
    30.3 @@ -39,7 +39,7 @@
    30.4  text {* Alternative induction rule. *}
    30.5  
    30.6  theorem fib_induct:
    30.7 -    "P 0 ==> P 1 ==> (!!n. P (n + 1) ==> P n ==> P (n + # 2)) ==> P (n::nat)"
    30.8 +    "P 0 ==> P 1 ==> (!!n. P (n + 1) ==> P n ==> P (n + 2)) ==> P (n::nat)"
    30.9    by (induct rule: fib.induct, simp+)
   30.10  
   30.11  
   30.12 @@ -56,7 +56,7 @@
   30.13    show "?P 0" by simp
   30.14    show "?P 1" by simp
   30.15    fix n
   30.16 -  have "fib (n + # 2 + k + 1)
   30.17 +  have "fib (n + 2 + k + 1)
   30.18      = fib (n + k + 1) + fib (n + 1 + k + 1)" by simp
   30.19    also assume "fib (n + k + 1)
   30.20      = fib (k + 1) * fib (n + 1) + fib k * fib n"
   30.21 @@ -65,9 +65,9 @@
   30.22      = fib (k + 1) * fib (n + 1 + 1) + fib k * fib (n + 1)"
   30.23        (is " _ = ?R2")
   30.24    also have "?R1 + ?R2
   30.25 -    = fib (k + 1) * fib (n + # 2 + 1) + fib k * fib (n + # 2)"
   30.26 +    = fib (k + 1) * fib (n + 2 + 1) + fib k * fib (n + 2)"
   30.27      by (simp add: add_mult_distrib2)
   30.28 -  finally show "?P (n + # 2)" .
   30.29 +  finally show "?P (n + 2)" .
   30.30  qed
   30.31  
   30.32  lemma gcd_fib_Suc_eq_1: "gcd (fib n, fib (n + 1)) = 1" (is "?P n")
   30.33 @@ -75,14 +75,14 @@
   30.34    show "?P 0" by simp
   30.35    show "?P 1" by simp
   30.36    fix n
   30.37 -  have "fib (n + # 2 + 1) = fib (n + 1) + fib (n + # 2)"
   30.38 +  have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)"
   30.39      by simp
   30.40 -  also have "gcd (fib (n + # 2), ...) = gcd (fib (n + # 2), fib (n + 1))"
   30.41 +  also have "gcd (fib (n + 2), ...) = gcd (fib (n + 2), fib (n + 1))"
   30.42      by (simp only: gcd_add2')
   30.43    also have "... = gcd (fib (n + 1), fib (n + 1 + 1))"
   30.44      by (simp add: gcd_commute)
   30.45    also assume "... = 1"
   30.46 -  finally show "?P (n + # 2)" .
   30.47 +  finally show "?P (n + 2)" .
   30.48  qed
   30.49  
   30.50  lemma gcd_mult_add: "0 < n ==> gcd (n * k + m, n) = gcd (m, n)"
    31.1 --- a/src/HOL/Isar_examples/HoareEx.thy	Fri Oct 05 23:58:52 2001 +0200
    31.2 +++ b/src/HOL/Isar_examples/HoareEx.thy	Sat Oct 06 00:02:46 2001 +0200
    31.3 @@ -39,7 +39,7 @@
    31.4  *}
    31.5  
    31.6  lemma
    31.7 -  "|- .{\<acute>(N_update (# 2 * \<acute>N)) : .{\<acute>N = # 10}.}. \<acute>N := # 2 * \<acute>N .{\<acute>N = # 10}."
    31.8 +  "|- .{\<acute>(N_update (2 * \<acute>N)) : .{\<acute>N = 10}.}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}."
    31.9    by (rule assign)
   31.10  
   31.11  text {*
   31.12 @@ -49,13 +49,13 @@
   31.13   ``obvious'' consequences as well.
   31.14  *}
   31.15  
   31.16 -lemma "|- .{True}. \<acute>N := # 10 .{\<acute>N = # 10}."
   31.17 +lemma "|- .{True}. \<acute>N := 10 .{\<acute>N = 10}."
   31.18    by hoare
   31.19  
   31.20 -lemma "|- .{# 2 * \<acute>N = # 10}. \<acute>N := # 2 * \<acute>N .{\<acute>N = # 10}."
   31.21 +lemma "|- .{2 * \<acute>N = 10}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}."
   31.22    by hoare
   31.23  
   31.24 -lemma "|- .{\<acute>N = # 5}. \<acute>N := # 2 * \<acute>N .{\<acute>N = # 10}."
   31.25 +lemma "|- .{\<acute>N = 5}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}."
   31.26    by hoare simp
   31.27  
   31.28  lemma "|- .{\<acute>N + 1 = a + 1}. \<acute>N := \<acute>N + 1 .{\<acute>N = a + 1}."
    32.1 --- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Fri Oct 05 23:58:52 2001 +0200
    32.2 +++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Sat Oct 06 00:02:46 2001 +0200
    32.3 @@ -76,7 +76,7 @@
    32.4    by (simp add: below_def less_Suc_eq) blast
    32.5  
    32.6  lemma Sigma_Suc2:
    32.7 -    "m = n + # 2 ==> A <*> below m =
    32.8 +    "m = n + 2 ==> A <*> below m =
    32.9        (A <*> {n}) Un (A <*> {n + 1}) Un (A <*> below n)"
   32.10    by (auto simp add: below_def) arith
   32.11  
   32.12 @@ -87,10 +87,10 @@
   32.13  
   32.14  constdefs
   32.15    evnodd :: "(nat * nat) set => nat => (nat * nat) set"
   32.16 -  "evnodd A b == A Int {(i, j). (i + j) mod # 2 = b}"
   32.17 +  "evnodd A b == A Int {(i, j). (i + j) mod 2 = b}"
   32.18  
   32.19  lemma evnodd_iff:
   32.20 -    "(i, j): evnodd A b = ((i, j): A  & (i + j) mod # 2 = b)"
   32.21 +    "(i, j): evnodd A b = ((i, j): A  & (i + j) mod 2 = b)"
   32.22    by (simp add: evnodd_def)
   32.23  
   32.24  lemma evnodd_subset: "evnodd A b <= A"
   32.25 @@ -112,7 +112,7 @@
   32.26    by (simp add: evnodd_def)
   32.27  
   32.28  lemma evnodd_insert: "evnodd (insert (i, j) C) b =
   32.29 -    (if (i + j) mod # 2 = b
   32.30 +    (if (i + j) mod 2 = b
   32.31        then insert (i, j) (evnodd C b) else evnodd C b)"
   32.32    by (simp add: evnodd_def) blast
   32.33  
   32.34 @@ -128,21 +128,21 @@
   32.35      vertl: "{(i, j), (i + 1, j)} : domino"
   32.36  
   32.37  lemma dominoes_tile_row:
   32.38 -  "{i} <*> below (# 2 * n) : tiling domino"
   32.39 +  "{i} <*> below (2 * n) : tiling domino"
   32.40    (is "?P n" is "?B n : ?T")
   32.41  proof (induct n)
   32.42    show "?P 0" by (simp add: below_0 tiling.empty)
   32.43  
   32.44    fix n assume hyp: "?P n"
   32.45 -  let ?a = "{i} <*> {# 2 * n + 1} Un {i} <*> {# 2 * n}"
   32.46 +  let ?a = "{i} <*> {2 * n + 1} Un {i} <*> {2 * n}"
   32.47  
   32.48    have "?B (Suc n) = ?a Un ?B n"
   32.49      by (auto simp add: Sigma_Suc Un_assoc)
   32.50    also have "... : ?T"
   32.51    proof (rule tiling.Un)
   32.52 -    have "{(i, # 2 * n), (i, # 2 * n + 1)} : domino"
   32.53 +    have "{(i, 2 * n), (i, 2 * n + 1)} : domino"
   32.54        by (rule domino.horiz)
   32.55 -    also have "{(i, # 2 * n), (i, # 2 * n + 1)} = ?a" by blast
   32.56 +    also have "{(i, 2 * n), (i, 2 * n + 1)} = ?a" by blast
   32.57      finally show "... : domino" .
   32.58      from hyp show "?B n : ?T" .
   32.59      show "?a <= - ?B n" by blast
   32.60 @@ -151,13 +151,13 @@
   32.61  qed
   32.62  
   32.63  lemma dominoes_tile_matrix:
   32.64 -  "below m <*> below (# 2 * n) : tiling domino"
   32.65 +  "below m <*> below (2 * n) : tiling domino"
   32.66    (is "?P m" is "?B m : ?T")
   32.67  proof (induct m)
   32.68    show "?P 0" by (simp add: below_0 tiling.empty)
   32.69  
   32.70    fix m assume hyp: "?P m"
   32.71 -  let ?t = "{m} <*> below (# 2 * n)"
   32.72 +  let ?t = "{m} <*> below (2 * n)"
   32.73  
   32.74    have "?B (Suc m) = ?t Un ?B m" by (simp add: Sigma_Suc)
   32.75    also have "... : ?T"
   32.76 @@ -170,9 +170,9 @@
   32.77  qed
   32.78  
   32.79  lemma domino_singleton:
   32.80 -  "d : domino ==> b < # 2 ==> EX i j. evnodd d b = {(i, j)}"
   32.81 +  "d : domino ==> b < 2 ==> EX i j. evnodd d b = {(i, j)}"
   32.82  proof -
   32.83 -  assume b: "b < # 2"
   32.84 +  assume b: "b < 2"
   32.85    assume "d : domino"
   32.86    thus ?thesis (is "?P d")
   32.87    proof induct
   32.88 @@ -227,9 +227,9 @@
   32.89        and at: "a <= - t"
   32.90  
   32.91      have card_suc:
   32.92 -      "!!b. b < # 2 ==> card (?e (a Un t) b) = Suc (card (?e t b))"
   32.93 +      "!!b. b < 2 ==> card (?e (a Un t) b) = Suc (card (?e t b))"
   32.94      proof -
   32.95 -      fix b :: nat assume "b < # 2"
   32.96 +      fix b :: nat assume "b < 2"
   32.97        have "?e (a Un t) b = ?e a b Un ?e t b" by (rule evnodd_Un)
   32.98        also obtain i j where e: "?e a b = {(i, j)}"
   32.99        proof -
  32.100 @@ -260,15 +260,15 @@
  32.101  constdefs
  32.102    mutilated_board :: "nat => nat => (nat * nat) set"
  32.103    "mutilated_board m n ==
  32.104 -    below (# 2 * (m + 1)) <*> below (# 2 * (n + 1))
  32.105 -      - {(0, 0)} - {(# 2 * m + 1, # 2 * n + 1)}"
  32.106 +    below (2 * (m + 1)) <*> below (2 * (n + 1))
  32.107 +      - {(0, 0)} - {(2 * m + 1, 2 * n + 1)}"
  32.108  
  32.109  theorem mutil_not_tiling: "mutilated_board m n ~: tiling domino"
  32.110  proof (unfold mutilated_board_def)
  32.111    let ?T = "tiling domino"
  32.112 -  let ?t = "below (# 2 * (m + 1)) <*> below (# 2 * (n + 1))"
  32.113 +  let ?t = "below (2 * (m + 1)) <*> below (2 * (n + 1))"
  32.114    let ?t' = "?t - {(0, 0)}"
  32.115 -  let ?t'' = "?t' - {(# 2 * m + 1, # 2 * n + 1)}"
  32.116 +  let ?t'' = "?t' - {(2 * m + 1, 2 * n + 1)}"
  32.117  
  32.118    show "?t'' ~: ?T"
  32.119    proof
  32.120 @@ -282,12 +282,12 @@
  32.121      note [simp] = evnodd_iff evnodd_empty evnodd_insert evnodd_Diff
  32.122      have "card (?e ?t'' 0) < card (?e ?t' 0)"
  32.123      proof -
  32.124 -      have "card (?e ?t' 0 - {(# 2 * m + 1, # 2 * n + 1)})
  32.125 +      have "card (?e ?t' 0 - {(2 * m + 1, 2 * n + 1)})
  32.126          < card (?e ?t' 0)"
  32.127        proof (rule card_Diff1_less)
  32.128          from _ fin show "finite (?e ?t' 0)"
  32.129            by (rule finite_subset) auto
  32.130 -        show "(# 2 * m + 1, # 2 * n + 1) : ?e ?t' 0" by simp
  32.131 +        show "(2 * m + 1, 2 * n + 1) : ?e ?t' 0" by simp
  32.132        qed
  32.133        thus ?thesis by simp
  32.134      qed
    33.1 --- a/src/HOL/Isar_examples/Summation.thy	Fri Oct 05 23:58:52 2001 +0200
    33.2 +++ b/src/HOL/Isar_examples/Summation.thy	Sat Oct 06 00:02:46 2001 +0200
    33.3 @@ -31,14 +31,14 @@
    33.4  *}
    33.5  
    33.6  theorem sum_of_naturals:
    33.7 -  "# 2 * (\<Sum>i < n + 1. i) = n * (n + 1)"
    33.8 +  "2 * (\<Sum>i < n + 1. i) = n * (n + 1)"
    33.9    (is "?P n" is "?S n = _")
   33.10  proof (induct n)
   33.11    show "?P 0" by simp
   33.12  next
   33.13 -  fix n have "?S (n + 1) = ?S n + # 2 * (n + 1)" by simp
   33.14 +  fix n have "?S (n + 1) = ?S n + 2 * (n + 1)" by simp
   33.15    also assume "?S n = n * (n + 1)"
   33.16 -  also have "... + # 2 * (n + 1) = (n + 1) * (n + # 2)" by simp
   33.17 +  also have "... + 2 * (n + 1) = (n + 1) * (n + 2)" by simp
   33.18    finally show "?P (Suc n)" by simp
   33.19  qed
   33.20  
   33.21 @@ -86,14 +86,14 @@
   33.22  *}
   33.23  
   33.24  theorem sum_of_odds:
   33.25 -  "(\<Sum>i < n. # 2 * i + 1) = n^Suc (Suc 0)"
   33.26 +  "(\<Sum>i < n. 2 * i + 1) = n^Suc (Suc 0)"
   33.27    (is "?P n" is "?S n = _")
   33.28  proof (induct n)
   33.29    show "?P 0" by simp
   33.30  next
   33.31 -  fix n have "?S (n + 1) = ?S n + # 2 * n + 1" by simp
   33.32 +  fix n have "?S (n + 1) = ?S n + 2 * n + 1" by simp
   33.33    also assume "?S n = n^Suc (Suc 0)"
   33.34 -  also have "... + # 2 * n + 1 = (n + 1)^Suc (Suc 0)" by simp
   33.35 +  also have "... + 2 * n + 1 = (n + 1)^Suc (Suc 0)" by simp
   33.36    finally show "?P (Suc n)" by simp
   33.37  qed
   33.38  
   33.39 @@ -106,28 +106,28 @@
   33.40  lemmas distrib = add_mult_distrib add_mult_distrib2
   33.41  
   33.42  theorem sum_of_squares:
   33.43 -  "# 6 * (\<Sum>i < n + 1. i^Suc (Suc 0)) = n * (n + 1) * (# 2 * n + 1)"
   33.44 +  "6 * (\<Sum>i < n + 1. i^Suc (Suc 0)) = n * (n + 1) * (2 * n + 1)"
   33.45    (is "?P n" is "?S n = _")
   33.46  proof (induct n)
   33.47    show "?P 0" by simp
   33.48  next
   33.49 -  fix n have "?S (n + 1) = ?S n + # 6 * (n + 1)^Suc (Suc 0)" by (simp add: distrib)
   33.50 -  also assume "?S n = n * (n + 1) * (# 2 * n + 1)"
   33.51 -  also have "... + # 6 * (n + 1)^Suc (Suc 0) =
   33.52 -    (n + 1) * (n + # 2) * (# 2 * (n + 1) + 1)" by (simp add: distrib)
   33.53 +  fix n have "?S (n + 1) = ?S n + 6 * (n + 1)^Suc (Suc 0)" by (simp add: distrib)
   33.54 +  also assume "?S n = n * (n + 1) * (2 * n + 1)"
   33.55 +  also have "... + 6 * (n + 1)^Suc (Suc 0) =
   33.56 +    (n + 1) * (n + 2) * (2 * (n + 1) + 1)" by (simp add: distrib)
   33.57    finally show "?P (Suc n)" by simp
   33.58  qed
   33.59  
   33.60  theorem sum_of_cubes:
   33.61 -  "# 4 * (\<Sum>i < n + 1. i^# 3) = (n * (n + 1))^Suc (Suc 0)"
   33.62 +  "4 * (\<Sum>i < n + 1. i^3) = (n * (n + 1))^Suc (Suc 0)"
   33.63    (is "?P n" is "?S n = _")
   33.64  proof (induct n)
   33.65    show "?P 0" by (simp add: power_eq_if)
   33.66  next
   33.67 -  fix n have "?S (n + 1) = ?S n + # 4 * (n + 1)^# 3"
   33.68 +  fix n have "?S (n + 1) = ?S n + 4 * (n + 1)^3"
   33.69      by (simp add: power_eq_if distrib)
   33.70    also assume "?S n = (n * (n + 1))^Suc (Suc 0)"
   33.71 -  also have "... + # 4 * (n + 1)^# 3 = ((n + 1) * ((n + 1) + 1))^Suc (Suc 0)"
   33.72 +  also have "... + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^Suc (Suc 0)"
   33.73      by (simp add: power_eq_if distrib)
   33.74    finally show "?P (Suc n)" by simp
   33.75  qed
    34.1 --- a/src/HOL/Lambda/Type.thy	Fri Oct 05 23:58:52 2001 +0200
    34.2 +++ b/src/HOL/Lambda/Type.thy	Sat Oct 06 00:02:46 2001 +0200
    34.3 @@ -59,11 +59,11 @@
    34.4  
    34.5  subsection {* Some examples *}
    34.6  
    34.7 -lemma "e |- Abs (Abs (Abs (Var 1 $ (Var # 2 $ Var 1 $ Var 0)))) : ?T"
    34.8 +lemma "e |- Abs (Abs (Abs (Var 1 $ (Var 2 $ Var 1 $ Var 0)))) : ?T"
    34.9    apply force
   34.10    done
   34.11  
   34.12 -lemma "e |- Abs (Abs (Abs (Var # 2 $ Var 0 $ (Var 1 $ Var 0)))) : ?T"
   34.13 +lemma "e |- Abs (Abs (Abs (Var 2 $ Var 0 $ (Var 1 $ Var 0)))) : ?T"
   34.14    apply force
   34.15    done
   34.16  
    35.1 --- a/src/HOL/Library/While_Combinator.thy	Fri Oct 05 23:58:52 2001 +0200
    35.2 +++ b/src/HOL/Library/While_Combinator.thy	Sat Oct 06 00:02:46 2001 +0200
    35.3 @@ -135,14 +135,14 @@
    35.4   theory.}
    35.5  *}
    35.6  
    35.7 -theorem "P (lfp (\<lambda>N::int set. {Numeral0} \<union> {(n + # 2) mod # 6 | n. n \<in> N})) =
    35.8 -    P {Numeral0, # 4, # 2}"
    35.9 +theorem "P (lfp (\<lambda>N::int set. {Numeral0} \<union> {(n + 2) mod 6 | n. n \<in> N})) =
   35.10 +    P {Numeral0, 4, 2}"
   35.11  proof -
   35.12    have aux: "!!f A B. {f n | n. A n \<or> B n} = {f n | n. A n} \<union> {f n | n. B n}"
   35.13      apply blast
   35.14      done
   35.15    show ?thesis
   35.16 -    apply (subst lfp_conv_while [where ?U = "{Numeral0, Numeral1, # 2, # 3, # 4, # 5}"])
   35.17 +    apply (subst lfp_conv_while [where ?U = "{Numeral0, Numeral1, 2, 3, 4, 5}"])
   35.18         apply (rule monoI)
   35.19        apply blast
   35.20       apply simp
    36.1 --- a/src/HOL/NumberTheory/EulerFermat.thy	Fri Oct 05 23:58:52 2001 +0200
    36.2 +++ b/src/HOL/NumberTheory/EulerFermat.thy	Sat Oct 06 00:02:46 2001 +0200
    36.3 @@ -55,7 +55,7 @@
    36.4    zcongm :: "int => int => int => bool"
    36.5    "zcongm m == \<lambda>a b. zcong a b m"
    36.6  
    36.7 -lemma abs_eq_1_iff [iff]: "(abs z = (Numeral1::int)) = (z = Numeral1 \<or> z = # -1)"
    36.8 +lemma abs_eq_1_iff [iff]: "(abs z = (Numeral1::int)) = (z = Numeral1 \<or> z = -1)"
    36.9    -- {* LCP: not sure why this lemma is needed now *}
   36.10    apply (auto simp add: zabs_def)
   36.11    done
    37.1 --- a/src/HOL/NumberTheory/Fib.thy	Fri Oct 05 23:58:52 2001 +0200
    37.2 +++ b/src/HOL/NumberTheory/Fib.thy	Sat Oct 06 00:02:46 2001 +0200
    37.3 @@ -67,14 +67,14 @@
    37.4  *}
    37.5  
    37.6  lemma fib_Cassini: "int (fib (Suc (Suc n)) * fib n) =
    37.7 -  (if n mod # 2 = 0 then int (fib (Suc n) * fib (Suc n)) - Numeral1
    37.8 +  (if n mod 2 = 0 then int (fib (Suc n) * fib (Suc n)) - Numeral1
    37.9     else int (fib (Suc n) * fib (Suc n)) + Numeral1)"
   37.10    apply (induct n rule: fib.induct)
   37.11      apply (simp add: fib.Suc_Suc)
   37.12     apply (simp add: fib.Suc_Suc mod_Suc)
   37.13    apply (simp add: fib.Suc_Suc
   37.14      add_mult_distrib add_mult_distrib2 mod_Suc zmult_int [symmetric] zmult_ac)
   37.15 -  apply (subgoal_tac "x mod # 2 < # 2", arith)
   37.16 +  apply (subgoal_tac "x mod 2 < 2", arith)
   37.17    apply simp
   37.18    done
   37.19  
    38.1 --- a/src/HOL/NumberTheory/WilsonBij.thy	Fri Oct 05 23:58:52 2001 +0200
    38.2 +++ b/src/HOL/NumberTheory/WilsonBij.thy	Sat Oct 06 00:02:46 2001 +0200
    38.3 @@ -133,15 +133,15 @@
    38.4    apply auto
    38.5    done
    38.6  
    38.7 -lemma aux3: "x \<le> p - # 2 ==> x < (p::int)"
    38.8 +lemma aux3: "x \<le> p - 2 ==> x < (p::int)"
    38.9    apply auto
   38.10    done
   38.11  
   38.12 -lemma aux4: "x \<le> p - # 2 ==> x < (p::int)-Numeral1"
   38.13 +lemma aux4: "x \<le> p - 2 ==> x < (p::int)-Numeral1"
   38.14    apply auto
   38.15    done
   38.16  
   38.17 -lemma inv_inj: "p \<in> zprime ==> inj_on (inv p) (d22set (p - # 2))"
   38.18 +lemma inv_inj: "p \<in> zprime ==> inj_on (inv p) (d22set (p - 2))"
   38.19    apply (unfold inj_on_def)
   38.20    apply auto
   38.21    apply (rule zcong_zless_imp_eq)
   38.22 @@ -160,7 +160,7 @@
   38.23    done
   38.24  
   38.25  lemma inv_d22set_d22set:
   38.26 -    "p \<in> zprime ==> inv p ` d22set (p - # 2) = d22set (p - # 2)"
   38.27 +    "p \<in> zprime ==> inv p ` d22set (p - 2) = d22set (p - 2)"
   38.28    apply (rule endo_inj_surj)
   38.29      apply (rule d22set_fin)
   38.30     apply (erule_tac [2] inv_inj)
   38.31 @@ -173,9 +173,9 @@
   38.32    done
   38.33  
   38.34  lemma d22set_d22set_bij:
   38.35 -    "p \<in> zprime ==> (d22set (p - # 2), d22set (p - # 2)) \<in> bijR (reciR p)"
   38.36 +    "p \<in> zprime ==> (d22set (p - 2), d22set (p - 2)) \<in> bijR (reciR p)"
   38.37    apply (unfold reciR_def)
   38.38 -  apply (rule_tac s = "(d22set (p - # 2), inv p ` d22set (p - # 2))" in subst)
   38.39 +  apply (rule_tac s = "(d22set (p - 2), inv p ` d22set (p - 2))" in subst)
   38.40     apply (simp add: inv_d22set_d22set)
   38.41    apply (rule inj_func_bijR)
   38.42      apply (rule_tac [3] d22set_fin)
   38.43 @@ -187,7 +187,7 @@
   38.44           apply (auto intro: d22set_g_1 d22set_le aux2 aux3 aux4)
   38.45    done
   38.46  
   38.47 -lemma reciP_bijP: "p \<in> zprime ==> bijP (reciR p) (d22set (p - # 2))"
   38.48 +lemma reciP_bijP: "p \<in> zprime ==> bijP (reciR p) (d22set (p - 2))"
   38.49    apply (unfold reciR_def bijP_def)
   38.50    apply auto
   38.51    apply (rule d22set_mem)
   38.52 @@ -217,7 +217,7 @@
   38.53    apply auto
   38.54    done
   38.55  
   38.56 -lemma bijER_d22set: "p \<in> zprime ==> d22set (p - # 2) \<in> bijER (reciR p)"
   38.57 +lemma bijER_d22set: "p \<in> zprime ==> d22set (p - 2) \<in> bijER (reciR p)"
   38.58    apply (rule bijR_bijER)
   38.59       apply (erule d22set_d22set_bij)
   38.60      apply (erule reciP_bijP)
   38.61 @@ -245,12 +245,12 @@
   38.62     apply auto
   38.63    done
   38.64  
   38.65 -theorem Wilson_Bij: "p \<in> zprime ==> [zfact (p - Numeral1) = # -1] (mod p)"
   38.66 -  apply (subgoal_tac "zcong ((p - Numeral1) * zfact (p - # 2)) (# -1 * Numeral1) p")
   38.67 +theorem Wilson_Bij: "p \<in> zprime ==> [zfact (p - Numeral1) = -1] (mod p)"
   38.68 +  apply (subgoal_tac "zcong ((p - Numeral1) * zfact (p - 2)) (-1 * Numeral1) p")
   38.69     apply (rule_tac [2] zcong_zmult)
   38.70      apply (simp add: zprime_def)
   38.71      apply (subst zfact.simps)
   38.72 -    apply (rule_tac t = "p - Numeral1 - Numeral1" and s = "p - # 2" in subst)
   38.73 +    apply (rule_tac t = "p - Numeral1 - Numeral1" and s = "p - 2" in subst)
   38.74       apply auto
   38.75     apply (simp add: zcong_def)
   38.76    apply (subst d22set_prod_zfact [symmetric])
    39.1 --- a/src/HOL/NumberTheory/WilsonRuss.thy	Fri Oct 05 23:58:52 2001 +0200
    39.2 +++ b/src/HOL/NumberTheory/WilsonRuss.thy	Sat Oct 06 00:02:46 2001 +0200
    39.3 @@ -20,7 +20,7 @@
    39.4    wset :: "int * int => int set"
    39.5  
    39.6  defs
    39.7 -  inv_def: "inv p a == (a^(nat (p - # 2))) mod p"
    39.8 +  inv_def: "inv p a == (a^(nat (p - 2))) mod p"
    39.9  
   39.10  recdef wset
   39.11    "measure ((\<lambda>(a, p). nat a) :: int * int => nat)"
   39.12 @@ -32,7 +32,7 @@
   39.13  
   39.14  text {* \medskip @{term [source] inv} *}
   39.15  
   39.16 -lemma aux: "Numeral1 < m ==> Suc (nat (m - # 2)) = nat (m - Numeral1)"
   39.17 +lemma aux: "Numeral1 < m ==> Suc (nat (m - 2)) = nat (m - Numeral1)"
   39.18    apply (subst int_int_eq [symmetric])
   39.19    apply auto
   39.20    done
   39.21 @@ -137,8 +137,8 @@
   39.22    apply (simp add: pos_mod_bound)
   39.23    done
   39.24  
   39.25 -lemma aux: "# 5 \<le> p ==>
   39.26 -    nat (p - # 2) * nat (p - # 2) = Suc (nat (p - Numeral1) * nat (p - # 3))"
   39.27 +lemma aux: "5 \<le> p ==>
   39.28 +    nat (p - 2) * nat (p - 2) = Suc (nat (p - Numeral1) * nat (p - 3))"
   39.29    apply (subst int_int_eq [symmetric])
   39.30    apply (simp add: zmult_int [symmetric])
   39.31    apply (simp add: zdiff_zmult_distrib zdiff_zmult_distrib2)
   39.32 @@ -154,7 +154,7 @@
   39.33    done
   39.34  
   39.35  lemma inv_inv: "p \<in> zprime \<Longrightarrow>
   39.36 -    # 5 \<le> p \<Longrightarrow> Numeral0 < a \<Longrightarrow> a < p ==> inv p (inv p a) = a"
   39.37 +    5 \<le> p \<Longrightarrow> Numeral0 < a \<Longrightarrow> a < p ==> inv p (inv p a) = a"
   39.38    apply (unfold inv_def)
   39.39    apply (subst zpower_zmod)
   39.40    apply (subst zpower_zpower)
   39.41 @@ -165,7 +165,7 @@
   39.42        apply (subst zcong_zmod [symmetric])
   39.43        apply (subst aux)
   39.44         apply (subgoal_tac [2]
   39.45 -	 "zcong (a * a^(nat (p - Numeral1) * nat (p - # 3))) (a * Numeral1) p")
   39.46 +	 "zcong (a * a^(nat (p - Numeral1) * nat (p - 3))) (a * Numeral1) p")
   39.47          apply (rule_tac [3] zcong_zmult)
   39.48           apply (rule_tac [4] zcong_zpower_zmult)
   39.49           apply (erule_tac [4] Little_Fermat)
   39.50 @@ -256,7 +256,7 @@
   39.51    done
   39.52  
   39.53  lemma wset_mem_inv_mem [rule_format]:
   39.54 -  "p \<in> zprime --> # 5 \<le> p --> a < p - Numeral1 --> b \<in> wset (a, p)
   39.55 +  "p \<in> zprime --> 5 \<le> p --> a < p - Numeral1 --> b \<in> wset (a, p)
   39.56      --> inv p b \<in> wset (a, p)"
   39.57    apply (induct a p rule: wset_induct)
   39.58     apply auto
   39.59 @@ -274,7 +274,7 @@
   39.60    done
   39.61  
   39.62  lemma wset_inv_mem_mem:
   39.63 -  "p \<in> zprime \<Longrightarrow> # 5 \<le> p \<Longrightarrow> a < p - Numeral1 \<Longrightarrow> Numeral1 < b \<Longrightarrow> b < p - Numeral1
   39.64 +  "p \<in> zprime \<Longrightarrow> 5 \<le> p \<Longrightarrow> a < p - Numeral1 \<Longrightarrow> Numeral1 < b \<Longrightarrow> b < p - Numeral1
   39.65      \<Longrightarrow> inv p b \<in> wset (a, p) \<Longrightarrow> b \<in> wset (a, p)"
   39.66    apply (rule_tac s = "inv p (inv p b)" and t = b in subst)
   39.67     apply (rule_tac [2] wset_mem_inv_mem)
   39.68 @@ -292,7 +292,7 @@
   39.69  
   39.70  lemma wset_zcong_prod_1 [rule_format]:
   39.71    "p \<in> zprime -->
   39.72 -    # 5 \<le> p --> a < p - Numeral1 --> [setprod (wset (a, p)) = Numeral1] (mod p)"
   39.73 +    5 \<le> p --> a < p - Numeral1 --> [setprod (wset (a, p)) = Numeral1] (mod p)"
   39.74    apply (induct a p rule: wset_induct)
   39.75     prefer 2
   39.76     apply (subst wset.simps)
   39.77 @@ -314,7 +314,7 @@
   39.78      apply auto
   39.79    done
   39.80  
   39.81 -lemma d22set_eq_wset: "p \<in> zprime ==> d22set (p - # 2) = wset (p - # 2, p)"
   39.82 +lemma d22set_eq_wset: "p \<in> zprime ==> d22set (p - 2) = wset (p - 2, p)"
   39.83    apply safe
   39.84     apply (erule wset_mem)
   39.85       apply (rule_tac [2] d22set_g_1)
   39.86 @@ -323,7 +323,7 @@
   39.87        apply (erule_tac [4] wset_g_1)
   39.88         prefer 6
   39.89         apply (subst zle_add1_eq_le [symmetric])
   39.90 -       apply (subgoal_tac "p - # 2 + Numeral1 = p - Numeral1")
   39.91 +       apply (subgoal_tac "p - 2 + Numeral1 = p - Numeral1")
   39.92          apply (simp (no_asm_simp))
   39.93          apply (erule wset_less)
   39.94           apply auto
   39.95 @@ -332,36 +332,36 @@
   39.96  
   39.97  subsection {* Wilson *}
   39.98  
   39.99 -lemma prime_g_5: "p \<in> zprime \<Longrightarrow> p \<noteq> # 2 \<Longrightarrow> p \<noteq> # 3 ==> # 5 \<le> p"
  39.100 +lemma prime_g_5: "p \<in> zprime \<Longrightarrow> p \<noteq> 2 \<Longrightarrow> p \<noteq> 3 ==> 5 \<le> p"
  39.101    apply (unfold zprime_def dvd_def)
  39.102 -  apply (case_tac "p = # 4")
  39.103 +  apply (case_tac "p = 4")
  39.104     apply auto
  39.105     apply (rule notE)
  39.106      prefer 2
  39.107      apply assumption
  39.108     apply (simp (no_asm))
  39.109 -   apply (rule_tac x = "# 2" in exI)
  39.110 +   apply (rule_tac x = "2" in exI)
  39.111     apply safe
  39.112 -     apply (rule_tac x = "# 2" in exI)
  39.113 +     apply (rule_tac x = "2" in exI)
  39.114       apply auto
  39.115    apply arith
  39.116    done
  39.117  
  39.118  theorem Wilson_Russ:
  39.119 -    "p \<in> zprime ==> [zfact (p - Numeral1) = # -1] (mod p)"
  39.120 -  apply (subgoal_tac "[(p - Numeral1) * zfact (p - # 2) = # -1 * Numeral1] (mod p)")
  39.121 +    "p \<in> zprime ==> [zfact (p - Numeral1) = -1] (mod p)"
  39.122 +  apply (subgoal_tac "[(p - Numeral1) * zfact (p - 2) = -1 * Numeral1] (mod p)")
  39.123     apply (rule_tac [2] zcong_zmult)
  39.124      apply (simp only: zprime_def)
  39.125      apply (subst zfact.simps)
  39.126 -    apply (rule_tac t = "p - Numeral1 - Numeral1" and s = "p - # 2" in subst)
  39.127 +    apply (rule_tac t = "p - Numeral1 - Numeral1" and s = "p - 2" in subst)
  39.128       apply auto
  39.129     apply (simp only: zcong_def)
  39.130     apply (simp (no_asm_simp))
  39.131 -  apply (case_tac "p = # 2")
  39.132 +  apply (case_tac "p = 2")
  39.133     apply (simp add: zfact.simps)
  39.134 -  apply (case_tac "p = # 3")
  39.135 +  apply (case_tac "p = 3")
  39.136     apply (simp add: zfact.simps)
  39.137 -  apply (subgoal_tac "# 5 \<le> p")
  39.138 +  apply (subgoal_tac "5 \<le> p")
  39.139     apply (erule_tac [2] prime_g_5)
  39.140      apply (subst d22set_prod_zfact [symmetric])
  39.141      apply (subst d22set_eq_wset)
    40.1 --- a/src/HOL/Numeral.thy	Fri Oct 05 23:58:52 2001 +0200
    40.2 +++ b/src/HOL/Numeral.thy	Sat Oct 06 00:02:46 2001 +0200
    40.3 @@ -24,7 +24,7 @@
    40.4  
    40.5  syntax
    40.6    "_constify" :: "num => numeral"    ("_")
    40.7 -  "_Numeral" :: "numeral => 'a"    ("#_")
    40.8 +  "_Numeral" :: "numeral => 'a"    ("_")
    40.9    Numeral0 :: 'a
   40.10    Numeral1 :: 'a
   40.11  
    41.1 --- a/src/HOL/Real/HahnBanach/VectorSpace.thy	Fri Oct 05 23:58:52 2001 +0200
    41.2 +++ b/src/HOL/Real/HahnBanach/VectorSpace.thy	Sat Oct 06 00:02:46 2001 +0200
    41.3 @@ -86,7 +86,7 @@
    41.4    by (unfold is_vectorspace_def) simp
    41.5  
    41.6  lemma negate_eq2a:
    41.7 -  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> # -1 \<cdot> x = - x"
    41.8 +  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> -1 \<cdot> x = - x"
    41.9    by (unfold is_vectorspace_def) simp
   41.10  
   41.11  lemma diff_eq2:
    42.1 --- a/src/HOL/Real/RComplete.ML	Fri Oct 05 23:58:52 2001 +0200
    42.2 +++ b/src/HOL/Real/RComplete.ML	Sat Oct 06 00:02:46 2001 +0200
    42.3 @@ -8,7 +8,7 @@
    42.4  
    42.5  claset_ref() := claset() delWrapper "bspec";
    42.6  
    42.7 -Goal "x/# 2 + x/# 2 = (x::real)";
    42.8 +Goal "x/2 + x/2 = (x::real)";
    42.9  by (Simp_tac 1);
   42.10  qed "real_sum_of_halves";
   42.11  
    43.1 --- a/src/HOL/Real/RealArith0.ML	Fri Oct 05 23:58:52 2001 +0200
    43.2 +++ b/src/HOL/Real/RealArith0.ML	Sat Oct 06 00:02:46 2001 +0200
    43.3 @@ -276,34 +276,34 @@
    43.4  set trace_simp;
    43.5  fun test s = (Goal s; by (Simp_tac 1)); 
    43.6  
    43.7 -test "Numeral0 <= (y::real) * # -2";
    43.8 -test "# 9*x = # 12 * (y::real)";
    43.9 -test "(# 9*x) / (# 12 * (y::real)) = z";
   43.10 -test "# 9*x < # 12 * (y::real)";
   43.11 -test "# 9*x <= # 12 * (y::real)";
   43.12 +test "Numeral0 <= (y::real) * -2";
   43.13 +test "9*x = 12 * (y::real)";
   43.14 +test "(9*x) / (12 * (y::real)) = z";
   43.15 +test "9*x < 12 * (y::real)";
   43.16 +test "9*x <= 12 * (y::real)";
   43.17  
   43.18 -test "# -99*x = # 132 * (y::real)";
   43.19 -test "(# -99*x) / (# 132 * (y::real)) = z";
   43.20 -test "# -99*x < # 132 * (y::real)";
   43.21 -test "# -99*x <= # 132 * (y::real)";
   43.22 +test "-99*x = 132 * (y::real)";
   43.23 +test "(-99*x) / (132 * (y::real)) = z";
   43.24 +test "-99*x < 132 * (y::real)";
   43.25 +test "-99*x <= 132 * (y::real)";
   43.26  
   43.27 -test "# 999*x = # -396 * (y::real)";
   43.28 -test "(# 999*x) / (# -396 * (y::real)) = z";
   43.29 -test "# 999*x < # -396 * (y::real)";
   43.30 -test "# 999*x <= # -396 * (y::real)";
   43.31 +test "999*x = -396 * (y::real)";
   43.32 +test "(999*x) / (-396 * (y::real)) = z";
   43.33 +test "999*x < -396 * (y::real)";
   43.34 +test "999*x <= -396 * (y::real)";
   43.35  
   43.36 -test "# -99*x = # -81 * (y::real)";
   43.37 -test "(# -99*x) / (# -81 * (y::real)) = z";
   43.38 -test "# -99*x <= # -81 * (y::real)";
   43.39 -test "# -99*x < # -81 * (y::real)";
   43.40 +test "-99*x = -81 * (y::real)";
   43.41 +test "(-99*x) / (-81 * (y::real)) = z";
   43.42 +test "-99*x <= -81 * (y::real)";
   43.43 +test "-99*x < -81 * (y::real)";
   43.44  
   43.45 -test "# -2 * x = # -1 * (y::real)";
   43.46 -test "# -2 * x = -(y::real)";
   43.47 -test "(# -2 * x) / (# -1 * (y::real)) = z";
   43.48 -test "# -2 * x < -(y::real)";
   43.49 -test "# -2 * x <= # -1 * (y::real)";
   43.50 -test "-x < # -23 * (y::real)";
   43.51 -test "-x <= # -23 * (y::real)";
   43.52 +test "-2 * x = -1 * (y::real)";
   43.53 +test "-2 * x = -(y::real)";
   43.54 +test "(-2 * x) / (-1 * (y::real)) = z";
   43.55 +test "-2 * x < -(y::real)";
   43.56 +test "-2 * x <= -1 * (y::real)";
   43.57 +test "-x < -23 * (y::real)";
   43.58 +test "-x <= -23 * (y::real)";
   43.59  *)
   43.60  
   43.61  
   43.62 @@ -505,18 +505,18 @@
   43.63  qed "real_divide_1";
   43.64  Addsimps [real_divide_1];
   43.65  
   43.66 -Goal "x/# -1 = -(x::real)";
   43.67 +Goal "x/-1 = -(x::real)";
   43.68  by (Simp_tac 1); 
   43.69  qed "real_divide_minus1";
   43.70  Addsimps [real_divide_minus1];
   43.71  
   43.72 -Goal "# -1/(x::real) = - (Numeral1/x)";
   43.73 +Goal "-1/(x::real) = - (Numeral1/x)";
   43.74  by (simp_tac (simpset() addsimps [real_divide_def, real_minus_inverse]) 1); 
   43.75  qed "real_minus1_divide";
   43.76  Addsimps [real_minus1_divide];
   43.77  
   43.78  Goal "[| (Numeral0::real) < d1; Numeral0 < d2 |] ==> EX e. Numeral0 < e & e < d1 & e < d2";
   43.79 -by (res_inst_tac [("x","(min d1 d2)/# 2")] exI 1); 
   43.80 +by (res_inst_tac [("x","(min d1 d2)/2")] exI 1); 
   43.81  by (asm_simp_tac (simpset() addsimps [min_def]) 1); 
   43.82  qed "real_lbound_gt_zero";
   43.83  
   43.84 @@ -647,11 +647,11 @@
   43.85  
   43.86  (*** Density of the Reals ***)
   43.87  
   43.88 -Goal "x < y ==> x < (x+y) / (# 2::real)";
   43.89 +Goal "x < y ==> x < (x+y) / (2::real)";
   43.90  by Auto_tac;
   43.91  qed "real_less_half_sum";
   43.92  
   43.93 -Goal "x < y ==> (x+y)/(# 2::real) < y";
   43.94 +Goal "x < y ==> (x+y)/(2::real) < y";
   43.95  by Auto_tac;
   43.96  qed "real_gt_half_sum";
   43.97  
    44.1 --- a/src/HOL/Real/RealBin.ML	Fri Oct 05 23:58:52 2001 +0200
    44.2 +++ b/src/HOL/Real/RealBin.ML	Sat Oct 06 00:02:46 2001 +0200
    44.3 @@ -58,18 +58,18 @@
    44.4  
    44.5  Addsimps [mult_real_number_of];
    44.6  
    44.7 -Goal "(# 2::real) = Numeral1 + Numeral1";
    44.8 +Goal "(2::real) = Numeral1 + Numeral1";
    44.9  by (Simp_tac 1);
   44.10  val lemma = result();
   44.11  
   44.12  (*For specialist use: NOT as default simprules*)
   44.13 -Goal "# 2 * z = (z+z::real)";
   44.14 +Goal "2 * z = (z+z::real)";
   44.15  by (simp_tac (simpset ()
   44.16  	      addsimps [lemma, real_add_mult_distrib,
   44.17  			one_eq_numeral_1 RS sym]) 1);
   44.18  qed "real_mult_2";
   44.19  
   44.20 -Goal "z * # 2 = (z+z::real)";
   44.21 +Goal "z * 2 = (z+z::real)";
   44.22  by (stac real_mult_commute 1 THEN rtac real_mult_2 1);
   44.23  qed "real_mult_2_right";
   44.24  
   44.25 @@ -111,12 +111,12 @@
   44.26  
   44.27  (*** New versions of existing theorems involving 0, 1r ***)
   44.28  
   44.29 -Goal "- Numeral1 = (# -1::real)";
   44.30 +Goal "- Numeral1 = (-1::real)";
   44.31  by (Simp_tac 1);
   44.32  qed "minus_numeral_one";
   44.33  
   44.34  
   44.35 -(*Maps 0 to Numeral0 and 1r to Numeral1 and -1r to # -1*)
   44.36 +(*Maps 0 to Numeral0 and 1r to Numeral1 and -1r to -1*)
   44.37  val real_numeral_ss = 
   44.38      HOL_ss addsimps [zero_eq_numeral_0, one_eq_numeral_1, 
   44.39  		     minus_numeral_one];
   44.40 @@ -488,7 +488,7 @@
   44.41  structure CombineNumeralsData =
   44.42    struct
   44.43    val add		= op + : int*int -> int 
   44.44 -  val mk_sum    	= long_mk_sum    (*to work for e.g. # 2*x + # 3*x *)
   44.45 +  val mk_sum    	= long_mk_sum    (*to work for e.g. 2*x + 3*x *)
   44.46    val dest_sum		= dest_sum
   44.47    val mk_coeff		= mk_coeff
   44.48    val dest_coeff	= dest_coeff 1
   44.49 @@ -548,35 +548,35 @@
   44.50  set trace_simp;
   44.51  fun test s = (Goal s; by (Simp_tac 1)); 
   44.52  
   44.53 -test "l + # 2 + # 2 + # 2 + (l + # 2) + (oo + # 2) = (uu::real)";
   44.54 +test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::real)";
   44.55  
   44.56 -test "# 2*u = (u::real)";
   44.57 -test "(i + j + # 12 + (k::real)) - # 15 = y";
   44.58 -test "(i + j + # 12 + (k::real)) - # 5 = y";
   44.59 +test "2*u = (u::real)";
   44.60 +test "(i + j + 12 + (k::real)) - 15 = y";
   44.61 +test "(i + j + 12 + (k::real)) - 5 = y";
   44.62  
   44.63  test "y - b < (b::real)";
   44.64 -test "y - (# 3*b + c) < (b::real) - # 2*c";
   44.65 +test "y - (3*b + c) < (b::real) - 2*c";
   44.66  
   44.67 -test "(# 2*x - (u*v) + y) - v*# 3*u = (w::real)";
   44.68 -test "(# 2*x*u*v + (u*v)*# 4 + y) - v*u*# 4 = (w::real)";
   44.69 -test "(# 2*x*u*v + (u*v)*# 4 + y) - v*u = (w::real)";
   44.70 -test "u*v - (x*u*v + (u*v)*# 4 + y) = (w::real)";
   44.71 +test "(2*x - (u*v) + y) - v*3*u = (w::real)";
   44.72 +test "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::real)";
   44.73 +test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::real)";
   44.74 +test "u*v - (x*u*v + (u*v)*4 + y) = (w::real)";
   44.75  
   44.76 -test "(i + j + # 12 + (k::real)) = u + # 15 + y";
   44.77 -test "(i + j*# 2 + # 12 + (k::real)) = j + # 5 + y";
   44.78 +test "(i + j + 12 + (k::real)) = u + 15 + y";
   44.79 +test "(i + j*2 + 12 + (k::real)) = j + 5 + y";
   44.80  
   44.81 -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)";
   44.82 +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)";
   44.83  
   44.84  test "a + -(b+c) + b = (d::real)";
   44.85  test "a + -(b+c) - b = (d::real)";
   44.86  
   44.87  (*negative numerals*)
   44.88 -test "(i + j + # -2 + (k::real)) - (u + # 5 + y) = zz";
   44.89 -test "(i + j + # -3 + (k::real)) < u + # 5 + y";
   44.90 -test "(i + j + # 3 + (k::real)) < u + # -6 + y";
   44.91 -test "(i + j + # -12 + (k::real)) - # 15 = y";
   44.92 -test "(i + j + # 12 + (k::real)) - # -15 = y";
   44.93 -test "(i + j + # -12 + (k::real)) - # -15 = y";
   44.94 +test "(i + j + -2 + (k::real)) - (u + 5 + y) = zz";
   44.95 +test "(i + j + -3 + (k::real)) < u + 5 + y";
   44.96 +test "(i + j + 3 + (k::real)) < u + -6 + y";
   44.97 +test "(i + j + -12 + (k::real)) - 15 = y";
   44.98 +test "(i + j + 12 + (k::real)) - -15 = y";
   44.99 +test "(i + j + -12 + (k::real)) - -15 = y";
  44.100  *)
  44.101  
  44.102  
    45.1 --- a/src/HOL/Real/RealPow.ML	Fri Oct 05 23:58:52 2001 +0200
    45.2 +++ b/src/HOL/Real/RealPow.ML	Sat Oct 06 00:02:46 2001 +0200
    45.3 @@ -76,7 +76,7 @@
    45.4  qed "realpow_eq_one";
    45.5  Addsimps [realpow_eq_one];
    45.6  
    45.7 -Goal "abs((# -1) ^ n) = (Numeral1::real)";
    45.8 +Goal "abs((-1) ^ n) = (Numeral1::real)";
    45.9  by (induct_tac "n" 1);
   45.10  by (auto_tac (claset(), simpset() addsimps [abs_mult]));
   45.11  qed "abs_realpow_minus_one";
   45.12 @@ -127,13 +127,13 @@
   45.13  by (auto_tac (claset() addDs [realpow_ge_one], simpset()));
   45.14  qed "realpow_ge_one2";
   45.15  
   45.16 -Goal "(Numeral1::real) <= # 2 ^ n";
   45.17 +Goal "(Numeral1::real) <= 2 ^ n";
   45.18  by (res_inst_tac [("y","Numeral1 ^ n")] order_trans 1);
   45.19  by (rtac realpow_le 2);
   45.20  by (auto_tac (claset() addIs [order_less_imp_le], simpset()));
   45.21  qed "two_realpow_ge_one";
   45.22  
   45.23 -Goal "real (n::nat) < # 2 ^ n";
   45.24 +Goal "real (n::nat) < 2 ^ n";
   45.25  by (induct_tac "n" 1);
   45.26  by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc]));
   45.27  by (stac real_mult_2 1);
   45.28 @@ -142,18 +142,18 @@
   45.29  qed "two_realpow_gt";
   45.30  Addsimps [two_realpow_gt,two_realpow_ge_one];
   45.31  
   45.32 -Goal "(# -1) ^ (# 2*n) = (Numeral1::real)";
   45.33 +Goal "(-1) ^ (2*n) = (Numeral1::real)";
   45.34  by (induct_tac "n" 1);
   45.35  by Auto_tac;
   45.36  qed "realpow_minus_one";
   45.37  Addsimps [realpow_minus_one];
   45.38  
   45.39 -Goal "(# -1) ^ Suc (# 2*n) = -(Numeral1::real)";
   45.40 +Goal "(-1) ^ Suc (2*n) = -(Numeral1::real)";
   45.41  by Auto_tac;
   45.42  qed "realpow_minus_one_odd";
   45.43  Addsimps [realpow_minus_one_odd];
   45.44  
   45.45 -Goal "(# -1) ^ Suc (Suc (# 2*n)) = (Numeral1::real)";
   45.46 +Goal "(-1) ^ Suc (Suc (2*n)) = (Numeral1::real)";
   45.47  by Auto_tac;
   45.48  qed "realpow_minus_one_even";
   45.49  Addsimps [realpow_minus_one_even];
    46.1 --- a/src/HOL/Real/ex/BinEx.thy	Fri Oct 05 23:58:52 2001 +0200
    46.2 +++ b/src/HOL/Real/ex/BinEx.thy	Sat Oct 06 00:02:46 2001 +0200
    46.3 @@ -15,52 +15,52 @@
    46.4  
    46.5  text {* \medskip Addition *}
    46.6  
    46.7 -lemma "(# 1359::real) + # -2468 = # -1109"
    46.8 +lemma "(1359::real) + -2468 = -1109"
    46.9    by simp
   46.10  
   46.11 -lemma "(# 93746::real) + # -46375 = # 47371"
   46.12 +lemma "(93746::real) + -46375 = 47371"
   46.13    by simp
   46.14  
   46.15  
   46.16  text {* \medskip Negation *}
   46.17  
   46.18 -lemma "- (# 65745::real) = # -65745"
   46.19 +lemma "- (65745::real) = -65745"
   46.20    by simp
   46.21  
   46.22 -lemma "- (# -54321::real) = # 54321"
   46.23 +lemma "- (-54321::real) = 54321"
   46.24    by simp
   46.25  
   46.26  
   46.27  text {* \medskip Multiplication *}
   46.28  
   46.29 -lemma "(# -84::real) * # 51 = # -4284"
   46.30 +lemma "(-84::real) * 51 = -4284"
   46.31    by simp
   46.32  
   46.33 -lemma "(# 255::real) * # 255 = # 65025"
   46.34 +lemma "(255::real) * 255 = 65025"
   46.35    by simp
   46.36  
   46.37 -lemma "(# 1359::real) * # -2468 = # -3354012"
   46.38 +lemma "(1359::real) * -2468 = -3354012"
   46.39    by simp
   46.40  
   46.41  
   46.42  text {* \medskip Inequalities *}
   46.43  
   46.44 -lemma "(# 89::real) * # 10 \<noteq> # 889"
   46.45 +lemma "(89::real) * 10 \<noteq> 889"
   46.46    by simp
   46.47  
   46.48 -lemma "(# 13::real) < # 18 - # 4"
   46.49 +lemma "(13::real) < 18 - 4"
   46.50    by simp
   46.51  
   46.52 -lemma "(# -345::real) < # -242 + # -100"
   46.53 +lemma "(-345::real) < -242 + -100"
   46.54    by simp
   46.55  
   46.56 -lemma "(# 13557456::real) < # 18678654"
   46.57 +lemma "(13557456::real) < 18678654"
   46.58    by simp
   46.59  
   46.60 -lemma "(# 999999::real) \<le> (# 1000001 + Numeral1)-# 2"
   46.61 +lemma "(999999::real) \<le> (1000001 + Numeral1) - 2"
   46.62    by simp
   46.63  
   46.64 -lemma "(# 1234567::real) \<le> # 1234567"
   46.65 +lemma "(1234567::real) \<le> 1234567"
   46.66    by simp
   46.67  
   46.68  
    47.1 --- a/src/HOL/Real/ex/Sqrt_Irrational.thy	Fri Oct 05 23:58:52 2001 +0200
    47.2 +++ b/src/HOL/Real/ex/Sqrt_Irrational.thy	Sat Oct 06 00:02:46 2001 +0200
    47.3 @@ -114,15 +114,15 @@
    47.4    this formally :-).
    47.5  *}
    47.6  
    47.7 -theorem "x\<twosuperior> = real (# 2::nat) ==> x \<notin> \<rat>"
    47.8 +theorem "x\<twosuperior> = real (2::nat) ==> x \<notin> \<rat>"
    47.9  proof (rule sqrt_prime_irrational)
   47.10    {
   47.11 -    fix m :: nat assume dvd: "m dvd # 2"
   47.12 -    hence "m \<le> # 2" by (simp add: dvd_imp_le)
   47.13 +    fix m :: nat assume dvd: "m dvd 2"
   47.14 +    hence "m \<le> 2" by (simp add: dvd_imp_le)
   47.15      moreover from dvd have "m \<noteq> 0" by (auto dest: dvd_0_left iff del: neq0_conv)
   47.16 -    ultimately have "m = 1 \<or> m = # 2" by arith
   47.17 +    ultimately have "m = 1 \<or> m = 2" by arith
   47.18    }
   47.19 -  thus "# 2 \<in> prime" by (simp add: prime_def)
   47.20 +  thus "2 \<in> prime" by (simp add: prime_def)
   47.21  qed
   47.22  
   47.23  text {*
    48.1 --- a/src/HOL/Real/real_arith0.ML	Fri Oct 05 23:58:52 2001 +0200
    48.2 +++ b/src/HOL/Real/real_arith0.ML	Sat Oct 06 00:02:46 2001 +0200
    48.3 @@ -118,7 +118,7 @@
    48.4  qed "";
    48.5  
    48.6  Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
    48.7 -\     ==> # 6*a <= # 5*l+i";
    48.8 +\     ==> 6*a <= 5*l+i";
    48.9  by (fast_arith_tac 1);
   48.10  qed "";
   48.11  *)
    49.1 --- a/src/HOL/UNITY/Simple/Mutex.ML	Fri Oct 05 23:58:52 2001 +0200
    49.2 +++ b/src/HOL/UNITY/Simple/Mutex.ML	Sat Oct 06 00:02:46 2001 +0200
    49.3 @@ -25,7 +25,7 @@
    49.4  qed "IV";
    49.5  
    49.6  (*The safety property: mutual exclusion*)
    49.7 -Goal "Mutex : Always {s. ~ (m s = # 3 & n s = # 3)}";
    49.8 +Goal "Mutex : Always {s. ~ (m s = 3 & n s = 3)}";
    49.9  by (rtac ([IU, IV] MRS Always_Int_I RS Always_weaken) 1);
   49.10  by Auto_tac;
   49.11  qed "mutual_exclusion";
   49.12 @@ -42,33 +42,33 @@
   49.13  getgoal 1;  
   49.14  
   49.15  
   49.16 -Goal "((Numeral1::int) <= i & i <= # 3) = (i = Numeral1 | i = # 2 | i = # 3)";
   49.17 +Goal "((Numeral1::int) <= i & i <= 3) = (i = Numeral1 | i = 2 | i = 3)";
   49.18  by (arith_tac 1);
   49.19  qed "eq_123";
   49.20  
   49.21  
   49.22  (*** Progress for U ***)
   49.23  
   49.24 -Goalw [Unless_def] "Mutex : {s. m s=# 2} Unless {s. m s=# 3}";
   49.25 +Goalw [Unless_def] "Mutex : {s. m s=2} Unless {s. m s=3}";
   49.26  by (constrains_tac 1);
   49.27  qed "U_F0";
   49.28  
   49.29 -Goal "Mutex : {s. m s=Numeral1} LeadsTo {s. p s = v s & m s = # 2}";
   49.30 +Goal "Mutex : {s. m s=Numeral1} LeadsTo {s. p s = v s & m s = 2}";
   49.31  by (ensures_tac "U1" 1);
   49.32  qed "U_F1";
   49.33  
   49.34 -Goal "Mutex : {s. ~ p s & m s = # 2} LeadsTo {s. m s = # 3}";
   49.35 +Goal "Mutex : {s. ~ p s & m s = 2} LeadsTo {s. m s = 3}";
   49.36  by (cut_facts_tac [IU] 1);
   49.37  by (ensures_tac "U2" 1);
   49.38  qed "U_F2";
   49.39  
   49.40 -Goal "Mutex : {s. m s = # 3} LeadsTo {s. p s}";
   49.41 -by (res_inst_tac [("B", "{s. m s = # 4}")] LeadsTo_Trans 1);
   49.42 +Goal "Mutex : {s. m s = 3} LeadsTo {s. p s}";
   49.43 +by (res_inst_tac [("B", "{s. m s = 4}")] LeadsTo_Trans 1);
   49.44  by (ensures_tac "U4" 2);
   49.45  by (ensures_tac "U3" 1);
   49.46  qed "U_F3";
   49.47  
   49.48 -Goal "Mutex : {s. m s = # 2} LeadsTo {s. p s}";
   49.49 +Goal "Mutex : {s. m s = 2} LeadsTo {s. p s}";
   49.50  by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo] 
   49.51  	  MRS LeadsTo_Diff) 1);
   49.52  by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1);
   49.53 @@ -80,7 +80,7 @@
   49.54  by (Blast_tac 1);
   49.55  val U_lemma1 = result();
   49.56  
   49.57 -Goal "Mutex : {s. Numeral1 <= m s & m s <= # 3} LeadsTo {s. p s}";
   49.58 +Goal "Mutex : {s. Numeral1 <= m s & m s <= 3} LeadsTo {s. p s}";
   49.59  by (simp_tac (simpset() addsimps [eq_123, Collect_disj_eq, LeadsTo_Un_distrib,
   49.60  				  U_lemma1, U_lemma2, U_F3] ) 1);
   49.61  val U_lemma123 = result();
   49.62 @@ -95,26 +95,26 @@
   49.63  (*** Progress for V ***)
   49.64  
   49.65  
   49.66 -Goalw [Unless_def] "Mutex : {s. n s=# 2} Unless {s. n s=# 3}";
   49.67 +Goalw [Unless_def] "Mutex : {s. n s=2} Unless {s. n s=3}";
   49.68  by (constrains_tac 1);
   49.69  qed "V_F0";
   49.70  
   49.71 -Goal "Mutex : {s. n s=Numeral1} LeadsTo {s. p s = (~ u s) & n s = # 2}";
   49.72 +Goal "Mutex : {s. n s=Numeral1} LeadsTo {s. p s = (~ u s) & n s = 2}";
   49.73  by (ensures_tac "V1" 1);
   49.74  qed "V_F1";
   49.75  
   49.76 -Goal "Mutex : {s. p s & n s = # 2} LeadsTo {s. n s = # 3}";
   49.77 +Goal "Mutex : {s. p s & n s = 2} LeadsTo {s. n s = 3}";
   49.78  by (cut_facts_tac [IV] 1);
   49.79  by (ensures_tac "V2" 1);
   49.80  qed "V_F2";
   49.81  
   49.82 -Goal "Mutex : {s. n s = # 3} LeadsTo {s. ~ p s}";
   49.83 -by (res_inst_tac [("B", "{s. n s = # 4}")] LeadsTo_Trans 1);
   49.84 +Goal "Mutex : {s. n s = 3} LeadsTo {s. ~ p s}";
   49.85 +by (res_inst_tac [("B", "{s. n s = 4}")] LeadsTo_Trans 1);
   49.86  by (ensures_tac "V4" 2);
   49.87  by (ensures_tac "V3" 1);
   49.88  qed "V_F3";
   49.89  
   49.90 -Goal "Mutex : {s. n s = # 2} LeadsTo {s. ~ p s}";
   49.91 +Goal "Mutex : {s. n s = 2} LeadsTo {s. ~ p s}";
   49.92  by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo] 
   49.93  	  MRS LeadsTo_Diff) 1);
   49.94  by (rtac ([V_F2, V_F3] MRS LeadsTo_Trans) 1);
   49.95 @@ -126,7 +126,7 @@
   49.96  by (Blast_tac 1);
   49.97  val V_lemma1 = result();
   49.98  
   49.99 -Goal "Mutex : {s. Numeral1 <= n s & n s <= # 3} LeadsTo {s. ~ p s}";
  49.100 +Goal "Mutex : {s. Numeral1 <= n s & n s <= 3} LeadsTo {s. ~ p s}";
  49.101  by (simp_tac (simpset() addsimps [eq_123, Collect_disj_eq, LeadsTo_Un_distrib,
  49.102  				  V_lemma1, V_lemma2, V_F3] ) 1);
  49.103  val V_lemma123 = result();
  49.104 @@ -142,7 +142,7 @@
  49.105  (** Absence of starvation **)
  49.106  
  49.107  (*Misra's F6*)
  49.108 -Goal "Mutex : {s. m s = Numeral1} LeadsTo {s. m s = # 3}";
  49.109 +Goal "Mutex : {s. m s = Numeral1} LeadsTo {s. m s = 3}";
  49.110  by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1);
  49.111  by (rtac U_F2 2);
  49.112  by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
  49.113 @@ -154,7 +154,7 @@
  49.114  qed "m1_Leadsto_3";
  49.115  
  49.116  (*The same for V*)
  49.117 -Goal "Mutex : {s. n s = Numeral1} LeadsTo {s. n s = # 3}";
  49.118 +Goal "Mutex : {s. n s = Numeral1} LeadsTo {s. n s = 3}";
  49.119  by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1);
  49.120  by (rtac V_F2 2);
  49.121  by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
    50.1 --- a/src/HOL/UNITY/Simple/Mutex.thy	Fri Oct 05 23:58:52 2001 +0200
    50.2 +++ b/src/HOL/UNITY/Simple/Mutex.thy	Sat Oct 06 00:02:46 2001 +0200
    50.3 @@ -25,16 +25,16 @@
    50.4      "U0 == {(s,s'). s' = s (|u:=True, m:=Numeral1|) & m s = Numeral0}"
    50.5  
    50.6    U1 :: command
    50.7 -    "U1 == {(s,s'). s' = s (|p:= v s, m:=# 2|) & m s = Numeral1}"
    50.8 +    "U1 == {(s,s'). s' = s (|p:= v s, m:=2|) & m s = Numeral1}"
    50.9  
   50.10    U2 :: command
   50.11 -    "U2 == {(s,s'). s' = s (|m:=# 3|) & ~ p s & m s = # 2}"
   50.12 +    "U2 == {(s,s'). s' = s (|m:=3|) & ~ p s & m s = 2}"
   50.13  
   50.14    U3 :: command
   50.15 -    "U3 == {(s,s'). s' = s (|u:=False, m:=# 4|) & m s = # 3}"
   50.16 +    "U3 == {(s,s'). s' = s (|u:=False, m:=4|) & m s = 3}"
   50.17  
   50.18    U4 :: command
   50.19 -    "U4 == {(s,s'). s' = s (|p:=True, m:=Numeral0|) & m s = # 4}"
   50.20 +    "U4 == {(s,s'). s' = s (|p:=True, m:=Numeral0|) & m s = 4}"
   50.21  
   50.22    (** The program for process V **)
   50.23    
   50.24 @@ -42,16 +42,16 @@
   50.25      "V0 == {(s,s'). s' = s (|v:=True, n:=Numeral1|) & n s = Numeral0}"
   50.26  
   50.27    V1 :: command
   50.28 -    "V1 == {(s,s'). s' = s (|p:= ~ u s, n:=# 2|) & n s = Numeral1}"
   50.29 +    "V1 == {(s,s'). s' = s (|p:= ~ u s, n:=2|) & n s = Numeral1}"
   50.30  
   50.31    V2 :: command
   50.32 -    "V2 == {(s,s'). s' = s (|n:=# 3|) & p s & n s = # 2}"
   50.33 +    "V2 == {(s,s'). s' = s (|n:=3|) & p s & n s = 2}"
   50.34  
   50.35    V3 :: command
   50.36 -    "V3 == {(s,s'). s' = s (|v:=False, n:=# 4|) & n s = # 3}"
   50.37 +    "V3 == {(s,s'). s' = s (|v:=False, n:=4|) & n s = 3}"
   50.38  
   50.39    V4 :: command
   50.40 -    "V4 == {(s,s'). s' = s (|p:=False, n:=Numeral0|) & n s = # 4}"
   50.41 +    "V4 == {(s,s'). s' = s (|p:=False, n:=Numeral0|) & n s = 4}"
   50.42  
   50.43    Mutex :: state program
   50.44      "Mutex == mk_program ({s. ~ u s & ~ v s & m s = Numeral0 & n s = Numeral0},
   50.45 @@ -62,15 +62,15 @@
   50.46    (** The correct invariants **)
   50.47  
   50.48    IU :: state set
   50.49 -    "IU == {s. (u s = (Numeral1 <= m s & m s <= # 3)) & (m s = # 3 --> ~ p s)}"
   50.50 +    "IU == {s. (u s = (Numeral1 <= m s & m s <= 3)) & (m s = 3 --> ~ p s)}"
   50.51  
   50.52    IV :: state set
   50.53 -    "IV == {s. (v s = (Numeral1 <= n s & n s <= # 3)) & (n s = # 3 --> p s)}"
   50.54 +    "IV == {s. (v s = (Numeral1 <= n s & n s <= 3)) & (n s = 3 --> p s)}"
   50.55  
   50.56    (** The faulty invariant (for U alone) **)
   50.57  
   50.58    bad_IU :: state set
   50.59 -    "bad_IU == {s. (u s = (Numeral1 <= m s & m s <= # 3)) &
   50.60 -	           (# 3 <= m s & m s <= # 4 --> ~ p s)}"
   50.61 +    "bad_IU == {s. (u s = (Numeral1 <= m s & m s <= 3)) &
   50.62 +	           (3 <= m s & m s <= 4 --> ~ p s)}"
   50.63  
   50.64  end
    51.1 --- a/src/HOL/UNITY/Union.ML	Fri Oct 05 23:58:52 2001 +0200
    51.2 +++ b/src/HOL/UNITY/Union.ML	Sat Oct 06 00:02:46 2001 +0200
    51.3 @@ -352,7 +352,7 @@
    51.4  
    51.5  bind_thm ("ok_sym", ok_commute RS iffD1);
    51.6  
    51.7 -Goal "OK {(Numeral0::int,F),(Numeral1,G),(# 2,H)} snd = (F ok G & (F Join G) ok H)";
    51.8 +Goal "OK {(Numeral0::int,F),(Numeral1,G),(2,H)} snd = (F ok G & (F Join G) ok H)";
    51.9  by (asm_full_simp_tac
   51.10      (simpset() addsimps [Ball_def, conj_disj_distribR, ok_def, Join_def, 
   51.11                     OK_def, insert_absorb, all_conj_distrib, eq_commute]) 1); 
    52.1 --- a/src/HOL/Unix/ROOT.ML	Fri Oct 05 23:58:52 2001 +0200
    52.2 +++ b/src/HOL/Unix/ROOT.ML	Sat Oct 06 00:02:46 2001 +0200
    52.3 @@ -1,3 +1,3 @@
    52.4  
    52.5 -Library.setmp print_mode (! print_mode @ ["no_brackets"])
    52.6 +Library.setmp print_mode (! print_mode @ ["no_brackets", "no_type_brackets"])
    52.7    use_thy "Unix";
    53.1 --- a/src/HOL/arith_data.ML	Fri Oct 05 23:58:52 2001 +0200
    53.2 +++ b/src/HOL/arith_data.ML	Sat Oct 06 00:02:46 2001 +0200
    53.3 @@ -438,7 +438,7 @@
    53.4    [Simplifier.change_simpset_of (op addSolver)
    53.5     (mk_solver "lin. arith." Fast_Arith.cut_lin_arith_tac),
    53.6    Simplifier.change_simpset_of (op addsimprocs) [fast_nat_arith_simproc],
    53.7 -  Method.add_methods [("arith", (arith_method o # 2) oo Method.syntax Args.bang_facts,
    53.8 +  Method.add_methods [("arith", (arith_method o #2) oo Method.syntax Args.bang_facts,
    53.9      "decide linear arithmethic")],
   53.10    Attrib.add_attributes [("arith_split",
   53.11      (Attrib.no_args arith_split_add, Attrib.no_args Attrib.undef_local_attribute),
    54.1 --- a/src/HOL/ex/BinEx.thy	Fri Oct 05 23:58:52 2001 +0200
    54.2 +++ b/src/HOL/ex/BinEx.thy	Sat Oct 06 00:02:46 2001 +0200
    54.3 @@ -12,75 +12,75 @@
    54.4  
    54.5  text {* Addition *}
    54.6  
    54.7 -lemma "(# 13::int) + # 19 = # 32"
    54.8 +lemma "(13::int) + 19 = 32"
    54.9    by simp
   54.10  
   54.11 -lemma "(# 1234::int) + # 5678 = # 6912"
   54.12 +lemma "(1234::int) + 5678 = 6912"
   54.13    by simp
   54.14  
   54.15 -lemma "(# 1359::int) + # -2468 = # -1109"
   54.16 +lemma "(1359::int) + -2468 = -1109"
   54.17    by simp
   54.18  
   54.19 -lemma "(# 93746::int) + # -46375 = # 47371"
   54.20 +lemma "(93746::int) + -46375 = 47371"
   54.21    by simp
   54.22  
   54.23  
   54.24  text {* \medskip Negation *}
   54.25  
   54.26 -lemma "- (# 65745::int) = # -65745"
   54.27 +lemma "- (65745::int) = -65745"
   54.28    by simp
   54.29  
   54.30 -lemma "- (# -54321::int) = # 54321"
   54.31 +lemma "- (-54321::int) = 54321"
   54.32    by simp
   54.33  
   54.34  
   54.35  text {* \medskip Multiplication *}
   54.36  
   54.37 -lemma "(# 13::int) * # 19 = # 247"
   54.38 +lemma "(13::int) * 19 = 247"
   54.39    by simp
   54.40  
   54.41 -lemma "(# -84::int) * # 51 = # -4284"
   54.42 +lemma "(-84::int) * 51 = -4284"
   54.43    by simp
   54.44  
   54.45 -lemma "(# 255::int) * # 255 = # 65025"
   54.46 +lemma "(255::int) * 255 = 65025"
   54.47    by simp
   54.48  
   54.49 -lemma "(# 1359::int) * # -2468 = # -3354012"
   54.50 +lemma "(1359::int) * -2468 = -3354012"
   54.51    by simp
   54.52  
   54.53 -lemma "(# 89::int) * # 10 \<noteq> # 889"
   54.54 +lemma "(89::int) * 10 \<noteq> 889"
   54.55    by simp
   54.56  
   54.57 -lemma "(# 13::int) < # 18 - # 4"
   54.58 +lemma "(13::int) < 18 - 4"
   54.59    by simp
   54.60  
   54.61 -lemma "(# -345::int) < # -242 + # -100"
   54.62 +lemma "(-345::int) < -242 + -100"
   54.63    by simp
   54.64  
   54.65 -lemma "(# 13557456::int) < # 18678654"
   54.66 +lemma "(13557456::int) < 18678654"
   54.67    by simp
   54.68  
   54.69 -lemma "(# 999999::int) \<le> (# 1000001 + Numeral1) - # 2"
   54.70 +lemma "(999999::int) \<le> (1000001 + Numeral1) - 2"
   54.71    by simp
   54.72  
   54.73 -lemma "(# 1234567::int) \<le> # 1234567"
   54.74 +lemma "(1234567::int) \<le> 1234567"
   54.75    by simp
   54.76  
   54.77  
   54.78  text {* \medskip Quotient and Remainder *}
   54.79  
   54.80 -lemma "(# 10::int) div # 3 = # 3"
   54.81 +lemma "(10::int) div 3 = 3"
   54.82    by simp
   54.83  
   54.84 -lemma "(# 10::int) mod # 3 = Numeral1"
   54.85 +lemma "(10::int) mod 3 = Numeral1"
   54.86    by simp
   54.87  
   54.88  text {* A negative divisor *}
   54.89  
   54.90 -lemma "(# 10::int) div # -3 = # -4"
   54.91 +lemma "(10::int) div -3 = -4"
   54.92    by simp
   54.93  
   54.94 -lemma "(# 10::int) mod # -3 = # -2"
   54.95 +lemma "(10::int) mod -3 = -2"
   54.96    by simp
   54.97  
   54.98  text {*
   54.99 @@ -88,50 +88,50 @@
  54.100    convention but not with the hardware of most computers}
  54.101  *}
  54.102  
  54.103 -lemma "(# -10::int) div # 3 = # -4"
  54.104 +lemma "(-10::int) div 3 = -4"
  54.105    by simp
  54.106  
  54.107 -lemma "(# -10::int) mod # 3 = # 2"
  54.108 +lemma "(-10::int) mod 3 = 2"
  54.109    by simp
  54.110  
  54.111  text {* A negative dividend \emph{and} divisor *}
  54.112  
  54.113 -lemma "(# -10::int) div # -3 = # 3"
  54.114 +lemma "(-10::int) div -3 = 3"
  54.115    by simp
  54.116  
  54.117 -lemma "(# -10::int) mod # -3 = # -1"
  54.118 +lemma "(-10::int) mod -3 = -1"
  54.119    by simp
  54.120  
  54.121  text {* A few bigger examples *}
  54.122  
  54.123 -lemma "(# 8452::int) mod # 3 = Numeral1"
  54.124 +lemma "(8452::int) mod 3 = Numeral1"
  54.125    by simp
  54.126  
  54.127 -lemma "(# 59485::int) div # 434 = # 137"
  54.128 +lemma "(59485::int) div 434 = 137"
  54.129    by simp
  54.130  
  54.131 -lemma "(# 1000006::int) mod # 10 = # 6"
  54.132 +lemma "(1000006::int) mod 10 = 6"
  54.133    by simp
  54.134  
  54.135  
  54.136  text {* \medskip Division by shifting *}
  54.137  
  54.138 -lemma "# 10000000 div # 2 = (# 5000000::int)"
  54.139 +lemma "10000000 div 2 = (5000000::int)"
  54.140    by simp
  54.141  
  54.142 -lemma "# 10000001 mod # 2 = (Numeral1::int)"
  54.143 +lemma "10000001 mod 2 = (Numeral1::int)"
  54.144    by simp
  54.145  
  54.146 -lemma "# 10000055 div # 32 = (# 312501::int)"
  54.147 +lemma "10000055 div 32 = (312501::int)"
  54.148    by simp
  54.149  
  54.150 -lemma "# 10000055 mod # 32 = (# 23::int)"
  54.151 +lemma "10000055 mod 32 = (23::int)"
  54.152    by simp
  54.153  
  54.154 -lemma "# 100094 div # 144 = (# 695::int)"
  54.155 +lemma "100094 div 144 = (695::int)"
  54.156    by simp
  54.157  
  54.158 -lemma "# 100094 mod # 144 = (# 14::int)"
  54.159 +lemma "100094 mod 144 = (14::int)"
  54.160    by simp
  54.161  
  54.162  
  54.163 @@ -139,65 +139,65 @@
  54.164  
  54.165  text {* Successor *}
  54.166  
  54.167 -lemma "Suc # 99999 = # 100000"
  54.168 +lemma "Suc 99999 = 100000"
  54.169    by (simp add: Suc_nat_number_of)
  54.170      -- {* not a default rewrite since sometimes we want to have @{text "Suc #nnn"} *}
  54.171  
  54.172  
  54.173  text {* \medskip Addition *}
  54.174  
  54.175 -lemma "(# 13::nat) + # 19 = # 32"
  54.176 +lemma "(13::nat) + 19 = 32"
  54.177    by simp
  54.178  
  54.179 -lemma "(# 1234::nat) + # 5678 = # 6912"
  54.180 +lemma "(1234::nat) + 5678 = 6912"
  54.181    by simp
  54.182  
  54.183 -lemma "(# 973646::nat) + # 6475 = # 980121"
  54.184 +lemma "(973646::nat) + 6475 = 980121"
  54.185    by simp
  54.186  
  54.187  
  54.188  text {* \medskip Subtraction *}
  54.189  
  54.190 -lemma "(# 32::nat) - # 14 = # 18"
  54.191 +lemma "(32::nat) - 14 = 18"
  54.192    by simp
  54.193  
  54.194 -lemma "(# 14::nat) - # 15 = Numeral0"
  54.195 +lemma "(14::nat) - 15 = Numeral0"
  54.196    by simp
  54.197  
  54.198 -lemma "(# 14::nat) - # 1576644 = Numeral0"
  54.199 +lemma "(14::nat) - 1576644 = Numeral0"
  54.200    by simp
  54.201  
  54.202 -lemma "(# 48273776::nat) - # 3873737 = # 44400039"
  54.203 +lemma "(48273776::nat) - 3873737 = 44400039"
  54.204    by simp
  54.205  
  54.206  
  54.207  text {* \medskip Multiplication *}
  54.208  
  54.209 -lemma "(# 12::nat) * # 11 = # 132"
  54.210 +lemma "(12::nat) * 11 = 132"
  54.211    by simp
  54.212  
  54.213 -lemma "(# 647::nat) * # 3643 = # 2357021"
  54.214 +lemma "(647::nat) * 3643 = 2357021"
  54.215    by simp
  54.216  
  54.217  
  54.218  text {* \medskip Quotient and Remainder *}
  54.219  
  54.220 -lemma "(# 10::nat) div # 3 = # 3"
  54.221 +lemma "(10::nat) div 3 = 3"
  54.222    by simp
  54.223  
  54.224 -lemma "(# 10::nat) mod # 3 = Numeral1"
  54.225 +lemma "(10::nat) mod 3 = Numeral1"
  54.226    by simp
  54.227  
  54.228 -lemma "(# 10000::nat) div # 9 = # 1111"
  54.229 +lemma "(10000::nat) div 9 = 1111"
  54.230    by simp
  54.231  
  54.232 -lemma "(# 10000::nat) mod # 9 = Numeral1"
  54.233 +lemma "(10000::nat) mod 9 = Numeral1"
  54.234    by simp
  54.235  
  54.236 -lemma "(# 10000::nat) div # 16 = # 625"
  54.237 +lemma "(10000::nat) div 16 = 625"
  54.238    by simp
  54.239  
  54.240 -lemma "(# 10000::nat) mod # 16 = Numeral0"
  54.241 +lemma "(10000::nat) mod 16 = Numeral0"
  54.242    by simp
  54.243  
  54.244  
    55.1 --- a/src/HOL/ex/NatSum.thy	Fri Oct 05 23:58:52 2001 +0200
    55.2 +++ b/src/HOL/ex/NatSum.thy	Sat Oct 06 00:02:46 2001 +0200
    55.3 @@ -36,8 +36,8 @@
    55.4  *}
    55.5  
    55.6  lemma sum_of_odd_squares:
    55.7 -  "# 3 * setsum (\<lambda>i. Suc (i + i) * Suc (i + i)) (lessThan n) =
    55.8 -    n * (# 4 * n * n - Numeral1)"
    55.9 +  "3 * setsum (\<lambda>i. Suc (i + i) * Suc (i + i)) (lessThan n) =
   55.10 +    n * (4 * n * n - Numeral1)"
   55.11    apply (induct n)
   55.12    txt {* This removes the @{term "-Numeral1"} from the inductive step *}
   55.13     apply (case_tac [2] n)
   55.14 @@ -51,7 +51,7 @@
   55.15  
   55.16  lemma sum_of_odd_cubes:
   55.17    "setsum (\<lambda>i. Suc (i + i) * Suc (i + i) * Suc (i + i)) (lessThan n) =
   55.18 -    n * n * (# 2 * n * n - Numeral1)"
   55.19 +    n * n * (2 * n * n - Numeral1)"
   55.20    apply (induct "n")
   55.21    txt {* This removes the @{term "-Numeral1"} from the inductive step *}
   55.22     apply (case_tac [2] "n")
   55.23 @@ -63,19 +63,19 @@
   55.24    @{text "n (n + 1) / 2"}.*}
   55.25  
   55.26  lemma sum_of_naturals:
   55.27 -    "# 2 * setsum id (atMost n) = n * Suc n"
   55.28 +    "2 * setsum id (atMost n) = n * Suc n"
   55.29    apply (induct n)
   55.30     apply auto
   55.31    done
   55.32  
   55.33  lemma sum_of_squares:
   55.34 -    "# 6 * setsum (\<lambda>i. i * i) (atMost n) = n * Suc n * Suc (# 2 * n)"
   55.35 +    "6 * setsum (\<lambda>i. i * i) (atMost n) = n * Suc n * Suc (2 * n)"
   55.36    apply (induct n)
   55.37     apply auto
   55.38    done
   55.39  
   55.40  lemma sum_of_cubes:
   55.41 -    "# 4 * setsum (\<lambda>i. i * i * i) (atMost n) = n * n * Suc n * Suc n"
   55.42 +    "4 * setsum (\<lambda>i. i * i * i) (atMost n) = n * n * Suc n * Suc n"
   55.43    apply (induct n)
   55.44     apply auto
   55.45    done
   55.46 @@ -86,8 +86,8 @@
   55.47  *}
   55.48  
   55.49  lemma sum_of_fourth_powers:
   55.50 -  "# 30 * setsum (\<lambda>i. i * i * i * i) (atMost n) =
   55.51 -    n * Suc n * Suc (# 2 * n) * (# 3 * n * n + # 3 * n - Numeral1)"
   55.52 +  "30 * setsum (\<lambda>i. i * i * i * i) (atMost n) =
   55.53 +    n * Suc n * Suc (2 * n) * (3 * n * n + 3 * n - Numeral1)"
   55.54    apply (induct n)
   55.55     apply auto
   55.56    txt {* Eliminates the subtraction *}
   55.57 @@ -107,9 +107,9 @@
   55.58    zdiff_zmult_distrib2 [simp]
   55.59  
   55.60  lemma int_sum_of_fourth_powers:
   55.61 -  "# 30 * int (setsum (\<lambda>i. i * i * i * i) (lessThan m)) =
   55.62 -    int m * (int m - Numeral1) * (int (# 2 * m) - Numeral1) *
   55.63 -    (int (# 3 * m * m) - int (# 3 * m) - Numeral1)"
   55.64 +  "30 * int (setsum (\<lambda>i. i * i * i * i) (lessThan m)) =
   55.65 +    int m * (int m - Numeral1) * (int (2 * m) - Numeral1) *
   55.66 +    (int (3 * m * m) - int (3 * m) - Numeral1)"
   55.67    apply (induct m)
   55.68     apply simp_all
   55.69    done
   55.70 @@ -118,12 +118,12 @@
   55.71  text {*
   55.72    \medskip Sums of geometric series: 2, 3 and the general case *}
   55.73  
   55.74 -lemma sum_of_2_powers: "setsum (\<lambda>i. # 2^i) (lessThan n) = # 2^n - (1::nat)"
   55.75 +lemma sum_of_2_powers: "setsum (\<lambda>i. 2^i) (lessThan n) = 2^n - (1::nat)"
   55.76    apply (induct n)
   55.77     apply (auto split: nat_diff_split) 
   55.78    done
   55.79  
   55.80 -lemma sum_of_3_powers: "# 2 * setsum (\<lambda>i. # 3^i) (lessThan n) = # 3^n - (1::nat)"
   55.81 +lemma sum_of_3_powers: "2 * setsum (\<lambda>i. 3^i) (lessThan n) = 3^n - (1::nat)"
   55.82    apply (induct n)
   55.83     apply auto
   55.84    done
    56.1 --- a/src/HOL/ex/Primrec.thy	Fri Oct 05 23:58:52 2001 +0200
    56.2 +++ b/src/HOL/ex/Primrec.thy	Sat Oct 06 00:02:46 2001 +0200
    56.3 @@ -159,7 +159,7 @@
    56.4  
    56.5  text {* PROPERTY A 8 *}
    56.6  
    56.7 -lemma ack_1 [simp]: "ack (Suc 0, j) = j + # 2"
    56.8 +lemma ack_1 [simp]: "ack (Suc 0, j) = j + 2"
    56.9    apply (induct j)
   56.10     apply simp_all
   56.11    done
   56.12 @@ -168,7 +168,7 @@
   56.13  text {* PROPERTY A 9.  The unary @{text 1} and @{text 2} in @{term
   56.14    ack} is essential for the rewriting. *}
   56.15  
   56.16 -lemma ack_2 [simp]: "ack (Suc (Suc 0), j) = # 2 * j + # 3"
   56.17 +lemma ack_2 [simp]: "ack (Suc (Suc 0), j) = 2 * j + 3"
   56.18    apply (induct j)
   56.19     apply simp_all
   56.20    done
   56.21 @@ -203,7 +203,7 @@
   56.22  
   56.23  text {* PROPERTY A 10 *}
   56.24  
   56.25 -lemma ack_nest_bound: "ack(i1, ack (i2, j)) < ack (# 2 + (i1 + i2), j)"
   56.26 +lemma ack_nest_bound: "ack(i1, ack (i2, j)) < ack (2 + (i1 + i2), j)"
   56.27    apply (simp add: numerals)
   56.28    apply (rule ack2_le_ack1 [THEN [2] less_le_trans])
   56.29    apply simp
   56.30 @@ -215,7 +215,7 @@
   56.31  
   56.32  text {* PROPERTY A 11 *}
   56.33  
   56.34 -lemma ack_add_bound: "ack (i1, j) + ack (i2, j) < ack (# 4 + (i1 + i2), j)"
   56.35 +lemma ack_add_bound: "ack (i1, j) + ack (i2, j) < ack (4 + (i1 + i2), j)"
   56.36    apply (rule_tac j = "ack (Suc (Suc 0), ack (i1 + i2, j))" in less_trans)
   56.37     prefer 2
   56.38     apply (rule ack_nest_bound [THEN less_le_trans])
   56.39 @@ -231,7 +231,7 @@
   56.40    used @{text "k + 4"}.  Quantified version must be nested @{text
   56.41    "\<exists>k'. \<forall>i j. ..."} *}
   56.42  
   56.43 -lemma ack_add_bound2: "i < ack (k, j) ==> i + j < ack (# 4 + k, j)"
   56.44 +lemma ack_add_bound2: "i < ack (k, j) ==> i + j < ack (4 + k, j)"
   56.45    apply (rule_tac j = "ack (k, j) + ack (0, j)" in less_trans)
   56.46     prefer 2
   56.47     apply (rule ack_add_bound [THEN less_le_trans])
    57.1 --- a/src/HOL/ex/Records.thy	Fri Oct 05 23:58:52 2001 +0200
    57.2 +++ b/src/HOL/ex/Records.thy	Sat Oct 06 00:02:46 2001 +0200
    57.3 @@ -182,7 +182,7 @@
    57.4  
    57.5  constdefs
    57.6    foo10 :: nat
    57.7 -  "foo10 == getX (| x = # 2, y = 0, colour = Blue |)"
    57.8 +  "foo10 == getX (| x = 2, y = 0, colour = Blue |)"
    57.9  
   57.10  
   57.11  subsubsection {* Non-coercive structural subtyping *}
   57.12 @@ -194,7 +194,7 @@
   57.13  
   57.14  constdefs
   57.15    foo11 :: cpoint
   57.16 -  "foo11 == setX (| x = # 2, y = 0, colour = Blue |) 0"
   57.17 +  "foo11 == setX (| x = 2, y = 0, colour = Blue |) 0"
   57.18  
   57.19  
   57.20  subsection {* Other features *}
   57.21 @@ -207,7 +207,7 @@
   57.22  
   57.23  text {*
   57.24   \noindent May not apply @{term getX} to 
   57.25 - @{term [source] "(| x' = # 2, y' = 0 |)"}.
   57.26 + @{term [source] "(| x' = 2, y' = 0 |)"}.
   57.27  *}
   57.28  
   57.29  text {* \medskip Polymorphic records. *}
    58.1 --- a/src/HOL/ex/svc_test.ML	Fri Oct 05 23:58:52 2001 +0200
    58.2 +++ b/src/HOL/ex/svc_test.ML	Sat Oct 06 00:02:46 2001 +0200
    58.3 @@ -231,9 +231,9 @@
    58.4  
    58.5  (** Linear arithmetic **)
    58.6  
    58.7 -Goal "x ~= # 14 & x ~= # 13 & x ~= # 12 & x ~= # 11 & x ~= # 10 & x ~= # 9 & \
    58.8 -\     x ~= # 8 & x ~= # 7 & x ~= # 6 & x ~= # 5 & x ~= # 4 & x ~= # 3 & \
    58.9 -\     x ~= # 2 & x ~= Numeral1 & Numeral0 < x & x < # 16 --> # 15 = (x::int)";
   58.10 +Goal "x ~= 14 & x ~= 13 & x ~= 12 & x ~= 11 & x ~= 10 & x ~= 9 & \
   58.11 +\     x ~= 8 & x ~= 7 & x ~= 6 & x ~= 5 & x ~= 4 & x ~= 3 & \
   58.12 +\     x ~= 2 & x ~= Numeral1 & Numeral0 < x & x < 16 --> 15 = (x::int)";
   58.13  by (svc_tac 1);
   58.14  qed "";
   58.15  
   58.16 @@ -244,11 +244,11 @@
   58.17  
   58.18  (** Natural number examples requiring implicit "non-negative" assumptions*)
   58.19  
   58.20 -Goal "(# 3::nat)*a <= # 2 + # 4*b + # 6*c  & # 11 <= # 2*a + b + # 2*c & \
   58.21 -\     a + # 3*b <= # 5 + # 2*c  --> # 2 + # 3*b <= # 2*a + # 6*c";
   58.22 +Goal "(3::nat)*a <= 2 + 4*b + 6*c  & 11 <= 2*a + b + 2*c & \
   58.23 +\     a + 3*b <= 5 + 2*c  --> 2 + 3*b <= 2*a + 6*c";
   58.24  by (svc_tac 1);
   58.25  qed "";
   58.26  
   58.27 -Goal "(n::nat) < # 2 ==> (n = Numeral0) | (n = Numeral1)";
   58.28 +Goal "(n::nat) < 2 ==> (n = Numeral0) | (n = Numeral1)";
   58.29  by (svc_tac 1);
   58.30  qed "";
    59.1 --- a/src/HOLCF/FOCUS/Buffer_adm.ML	Fri Oct 05 23:58:52 2001 +0200
    59.2 +++ b/src/HOLCF/FOCUS/Buffer_adm.ML	Sat Oct 06 00:02:46 2001 +0200
    59.3 @@ -110,7 +110,7 @@
    59.4  Goal "f:BufEq ==> ? l. !i x s. s:BufAC_Asm --> x << s --> Fin (l i) < #x --> \
    59.5  		\    (x,f\\<cdot>x):down_iterate BufAC_Cmt_F i --> \
    59.6  		\    (s,f\\<cdot>s):down_iterate BufAC_Cmt_F i";
    59.7 -by (res_inst_tac [("x","%i. # 2*i")] exI 1);
    59.8 +by (res_inst_tac [("x","%i. 2*i")] exI 1);
    59.9  by (rtac allI 1);
   59.10  by (nat_ind_tac "i" 1);
   59.11  by ( Simp_tac 1);
   59.12 @@ -129,10 +129,10 @@
   59.13         \\<lbrakk>f \\<in> BufEq;
   59.14            \\<forall>x s. s \\<in> BufAC_Asm \\<longrightarrow>
   59.15                  x \\<sqsubseteq> s \\<longrightarrow>
   59.16 -                Fin (# 2 * i) < #x \\<longrightarrow>
   59.17 +                Fin (2 * i) < #x \\<longrightarrow>
   59.18                  (x, f\\<cdot>x) \\<in> down_iterate BufAC_Cmt_F i \\<longrightarrow>
   59.19                  (s, f\\<cdot>s) \\<in> down_iterate BufAC_Cmt_F i;
   59.20 -          Md d\\<leadsto>\\<bullet>\\<leadsto>xa \\<in> BufAC_Asm; Fin (# 2 * i) < #ya; f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>ya) = d\\<leadsto>t;
   59.21 +          Md d\\<leadsto>\\<bullet>\\<leadsto>xa \\<in> BufAC_Asm; Fin (2 * i) < #ya; f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>ya) = d\\<leadsto>t;
   59.22            (ya, t) \\<in> down_iterate BufAC_Cmt_F i; ya \\<sqsubseteq> xa\\<rbrakk>
   59.23         \\<Longrightarrow> (xa, rt\\<cdot>(f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>xa))) \\<in> down_iterate BufAC_Cmt_F i
   59.24  *)
   59.25 @@ -147,11 +147,11 @@
   59.26  by (hyp_subst_tac 1);
   59.27  (*
   59.28   1. \\<And>i d xa ya t ff ffa.
   59.29 -       \\<lbrakk>f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>ya) = d\\<leadsto>ffa\\<cdot>ya; Fin (# 2 * i) < #ya;
   59.30 +       \\<lbrakk>f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>ya) = d\\<leadsto>ffa\\<cdot>ya; Fin (2 * i) < #ya;
   59.31            (ya, ffa\\<cdot>ya) \\<in> down_iterate BufAC_Cmt_F i; ya \\<sqsubseteq> xa; f \\<in> BufEq;
   59.32            \\<forall>x s. s \\<in> BufAC_Asm \\<longrightarrow>
   59.33                  x \\<sqsubseteq> s \\<longrightarrow>
   59.34 -                Fin (# 2 * i) < #x \\<longrightarrow>
   59.35 +                Fin (2 * i) < #x \\<longrightarrow>
   59.36                  (x, f\\<cdot>x) \\<in> down_iterate BufAC_Cmt_F i \\<longrightarrow>
   59.37                  (s, f\\<cdot>s) \\<in> down_iterate BufAC_Cmt_F i;
   59.38            xa \\<in> BufAC_Asm; ff \\<in> BufEq; ffa \\<in> BufEq\\<rbrakk>