# HG changeset patch
# User haftmann
# Date 1411311371 -7200
# Node ID 6d46ad54a2abeabe0a9d12d4c37004fe65d9bfb8
# Parent  24096e89c131649e54003d97f80ed0e897f7321b
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum

diff -r 24096e89c131 -r 6d46ad54a2ab NEWS
--- a/NEWS	Sun Sep 21 16:56:06 2014 +0200
+++ b/NEWS	Sun Sep 21 16:56:11 2014 +0200
@@ -20,6 +20,11 @@
 * Command "class_deps" takes optional sort arguments constraining
 the search space.
 
+* Lexical separation of signed and unsigend numerals: categories "num"
+and "float" are unsigend.  INCOMPATIBILITY: subtle change in precedence
+of numeral signs, particulary in expressions involving infix syntax like
+"(- 1) ^ n".
+
 
 *** HOL ***
 
diff -r 24096e89c131 -r 6d46ad54a2ab src/Doc/Isar_Ref/Inner_Syntax.thy
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Sun Sep 21 16:56:06 2014 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Sun Sep 21 16:56:11 2014 +0200
@@ -599,8 +599,8 @@
     @{syntax_def (inner) var} & = & @{syntax_ref var} \\
     @{syntax_def (inner) tid} & = & @{syntax_ref typefree} \\
     @{syntax_def (inner) tvar} & = & @{syntax_ref typevar} \\
-    @{syntax_def (inner) num_token} & = & @{syntax_ref nat}@{text "  |  "}@{verbatim "-"}@{syntax_ref nat} \\
-    @{syntax_def (inner) float_token} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat}@{text "  |  "}@{verbatim "-"}@{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\
+    @{syntax_def (inner) num_token} & = & @{syntax_ref nat} \\
+    @{syntax_def (inner) float_token} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\
     @{syntax_def (inner) xnum_token} & = & @{verbatim "#"}@{syntax_ref nat}@{text "  |  "}@{verbatim "#-"}@{syntax_ref nat} \\
     @{syntax_def (inner) str_token} & = & @{verbatim "''"} @{text "\<dots>"} @{verbatim "''"} \\
     @{syntax_def (inner) string_token} & = & @{verbatim "\""} @{text "\<dots>"} @{verbatim "\""} \\
diff -r 24096e89c131 -r 6d46ad54a2ab src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Sun Sep 21 16:56:11 2014 +0200
@@ -40,7 +40,7 @@
 lemma horner_schema:
   fixes f :: "nat \<Rightarrow> nat" and G :: "nat \<Rightarrow> nat \<Rightarrow> nat" and F :: "nat \<Rightarrow> nat"
   assumes f_Suc: "\<And>n. f (Suc n) = G ((F ^^ n) s) (f n)"
-  shows "horner F G n ((F ^^ j') s) (f j') x = (\<Sum> j = 0..< n. -1 ^ j * (1 / (f (j' + j))) * x ^ j)"
+  shows "horner F G n ((F ^^ j') s) (f j') x = (\<Sum> j = 0..< n. (- 1) ^ j * (1 / (f (j' + j))) * x ^ j)"
 proof (induct n arbitrary: j')
   case 0
   then show ?case by auto
@@ -86,8 +86,8 @@
     and lb_Suc: "\<And> n i k x. lb (Suc n) i k x = lapprox_rat prec 1 k - x * (ub n (F i) (G i k) x)"
     and ub_0: "\<And> i k x. ub 0 i k x = 0"
     and ub_Suc: "\<And> n i k x. ub (Suc n) i k x = rapprox_rat prec 1 k - x * (lb n (F i) (G i k) x)"
-  shows "(lb n ((F ^^ j') s) (f j') x) \<le> (\<Sum>j=0..<n. -1 ^ j * (1 / (f (j' + j))) * (x ^ j))" (is "?lb") and
-    "(\<Sum>j=0..<n. -1 ^ j * (1 / (f (j' + j))) * (x ^ j)) \<le> (ub n ((F ^^ j') s) (f j') x)" (is "?ub")
+  shows "(lb n ((F ^^ j') s) (f j') x) \<le> (\<Sum>j=0..<n. (- 1) ^ j * (1 / (f (j' + j))) * (x ^ j))" (is "?lb") and
+    "(\<Sum>j=0..<n. (- 1) ^ j * (1 / (f (j' + j))) * (x ^ j)) \<le> (ub n ((F ^^ j') s) (f j') x)" (is "?ub")
 proof -
   have "?lb  \<and> ?ub"
     using horner_bounds'[where lb=lb, OF `0 \<le> real x` f_Suc lb_0 lb_Suc ub_0 ub_Suc]
@@ -107,7 +107,7 @@
 proof -
   { fix x y z :: float have "x - y * z = x + - y * z" by simp } note diff_mult_minus = this
   have sum_eq: "(\<Sum>j=0..<n. (1 / (f (j' + j))) * real x ^ j) =
-    (\<Sum>j = 0..<n. -1 ^ j * (1 / (f (j' + j))) * real (- x) ^ j)"
+    (\<Sum>j = 0..<n. (- 1) ^ j * (1 / (f (j' + j))) * real (- x) ^ j)"
     by (auto simp add: field_simps power_mult_distrib[symmetric])
   have "0 \<le> real (-x)" using assms by auto
   from horner_bounds[where G=G and F=F and f=f and s=s and prec=prec
@@ -166,13 +166,13 @@
 fun sqrt_iteration :: "nat \<Rightarrow> nat \<Rightarrow> float \<Rightarrow> float" where
 "sqrt_iteration prec 0 x = Float 1 ((bitlen \<bar>mantissa x\<bar> + exponent x) div 2 + 1)" |
 "sqrt_iteration prec (Suc m) x = (let y = sqrt_iteration prec m x
-                                  in Float 1 -1 * (y + float_divr prec x y))"
+                                  in Float 1 (- 1) * (y + float_divr prec x y))"
 
 lemma compute_sqrt_iteration_base[code]:
   shows "sqrt_iteration prec n (Float m e) =
     (if n = 0 then Float 1 ((if m = 0 then 0 else bitlen \<bar>m\<bar> + e) div 2 + 1)
     else (let y = sqrt_iteration prec (n - 1) (Float m e) in
-      Float 1 -1 * (y + float_divr prec (Float m e) y)))"
+      Float 1 (- 1) * (y + float_divr prec (Float m e) y)))"
   using bitlen_Float by (cases n) simp_all
 
 function ub_sqrt lb_sqrt :: "nat \<Rightarrow> float \<Rightarrow> float" where
@@ -262,7 +262,7 @@
   also have "\<dots> < real ?b" using Suc .
   finally have "sqrt x < (?b + x / ?b)/2" using sqrt_ub_pos_pos_1[OF Suc _ `0 < real x`] by auto
   also have "\<dots> \<le> (?b + (float_divr prec x ?b))/2" by (rule divide_right_mono, auto simp add: float_divr)
-  also have "\<dots> = (Float 1 -1) * (?b + (float_divr prec x ?b))" by simp
+  also have "\<dots> = (Float 1 (- 1)) * (?b + (float_divr prec x ?b))" by simp
   finally show ?case unfolding sqrt_iteration.simps Let_def distrib_left .
 qed
 
@@ -359,7 +359,7 @@
   assumes "0 \<le> real x" "real x \<le> 1" and "even n"
   shows "arctan x \<in> {(x * lb_arctan_horner prec n 1 (x * x)) .. (x * ub_arctan_horner prec (Suc n) 1 (x * x))}"
 proof -
-  let ?c = "\<lambda>i. -1^i * (1 / (i * 2 + (1::nat)) * real x ^ (i * 2 + 1))"
+  let ?c = "\<lambda>i. (- 1) ^ i * (1 / (i * 2 + (1::nat)) * real x ^ (i * 2 + 1))"
   let ?S = "\<lambda>n. \<Sum> i=0..<n. ?c i"
 
   have "0 \<le> real (x * x)" by auto
@@ -471,20 +471,20 @@
   "lb_arctan prec x = (let ub_horner = \<lambda> x. x * ub_arctan_horner prec (get_odd (prec div 4 + 1)) 1 (x * x) ;
                            lb_horner = \<lambda> x. x * lb_arctan_horner prec (get_even (prec div 4 + 1)) 1 (x * x)
     in (if x < 0          then - ub_arctan prec (-x) else
-        if x \<le> Float 1 -1 then lb_horner x else
+        if x \<le> Float 1 (- 1) then lb_horner x else
         if x \<le> Float 1 1  then Float 1 1 * lb_horner (float_divl prec x (1 + ub_sqrt prec (1 + x * x)))
                           else (let inv = float_divr prec 1 x
                                 in if inv > 1 then 0
-                                              else lb_pi prec * Float 1 -1 - ub_horner inv)))"
+                                              else lb_pi prec * Float 1 (- 1) - ub_horner inv)))"
 
 | "ub_arctan prec x = (let lb_horner = \<lambda> x. x * lb_arctan_horner prec (get_even (prec div 4 + 1)) 1 (x * x) ;
                            ub_horner = \<lambda> x. x * ub_arctan_horner prec (get_odd (prec div 4 + 1)) 1 (x * x)
     in (if x < 0          then - lb_arctan prec (-x) else
-        if x \<le> Float 1 -1 then ub_horner x else
+        if x \<le> Float 1 (- 1) then ub_horner x else
         if x \<le> Float 1 1  then let y = float_divr prec x (1 + lb_sqrt prec (1 + x * x))
-                               in if y > 1 then ub_pi prec * Float 1 -1
+                               in if y > 1 then ub_pi prec * Float 1 (- 1)
                                            else Float 1 1 * ub_horner y
-                          else ub_pi prec * Float 1 -1 - lb_horner (float_divl prec 1 x)))"
+                          else ub_pi prec * Float 1 (- 1) - lb_horner (float_divl prec 1 x)))"
 by pat_completeness auto
 termination by (relation "measure (\<lambda> v. let (prec, x) = case_sum id id v in (if x < 0 then 1 else 0))", auto)
 
@@ -499,7 +499,7 @@
     and "?lb_horner x" = "x * lb_arctan_horner prec (get_even (prec div 4 + 1)) 1 (x * x)"
 
   show ?thesis
-  proof (cases "x \<le> Float 1 -1")
+  proof (cases "x \<le> Float 1 (- 1)")
     case True hence "real x \<le> 1" by auto
     show ?thesis unfolding lb_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_P[OF True]
       using arctan_0_1_bounds[OF `0 \<le> real x` `real x \<le> 1`] by auto
@@ -543,7 +543,7 @@
       also have "\<dots> \<le> 2 * arctan (x / ?R)"
         using arctan_monotone'[OF monotone] by (auto intro!: mult_left_mono)
       also have "2 * arctan (x / ?R) = arctan x" using arctan_half[symmetric] unfolding numeral_2_eq_2 power_Suc2 power_0 mult_1_left .
-      finally show ?thesis unfolding lb_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 -1`] if_P[OF True] .
+      finally show ?thesis unfolding lb_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 (- 1)`] if_P[OF True] .
     next
       case False
       hence "2 < real x" by auto
@@ -555,7 +555,7 @@
       show ?thesis
       proof (cases "1 < ?invx")
         case True
-        show ?thesis unfolding lb_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 -1`] if_not_P[OF False] if_P[OF True]
+        show ?thesis unfolding lb_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 (- 1)`] if_not_P[OF False] if_P[OF True]
           using `0 \<le> arctan x` by auto
       next
         case False
@@ -570,10 +570,10 @@
           using `0 \<le> arctan x` arctan_inverse[OF `1 / x \<noteq> 0`]
           unfolding real_sgn_pos[OF `0 < 1 / real x`] le_diff_eq by auto
         moreover
-        have "lb_pi prec * Float 1 -1 \<le> pi / 2"
+        have "lb_pi prec * Float 1 (- 1) \<le> pi / 2"
           unfolding Float_num times_divide_eq_right mult_1_left using pi_boundaries by simp
         ultimately
-        show ?thesis unfolding lb_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 -1`] if_not_P[OF `\<not> x \<le> Float 1 1`] if_not_P[OF False]
+        show ?thesis unfolding lb_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 (- 1)`] if_not_P[OF `\<not> x \<le> Float 1 1`] if_not_P[OF False]
           by auto
       qed
     qed
@@ -589,7 +589,7 @@
     and "?lb_horner x" = "x * lb_arctan_horner prec (get_even (prec div 4 + 1)) 1 (x * x)"
 
   show ?thesis
-  proof (cases "x \<le> Float 1 -1")
+  proof (cases "x \<le> Float 1 (- 1)")
     case True hence "real x \<le> 1" by auto
     show ?thesis unfolding ub_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_P[OF True]
       using arctan_0_1_bounds[OF `0 \<le> real x` `real x \<le> 1`] by auto
@@ -623,9 +623,9 @@
       show ?thesis
       proof (cases "?DIV > 1")
         case True
-        have "pi / 2 \<le> ub_pi prec * Float 1 -1" unfolding Float_num times_divide_eq_right mult_1_left using pi_boundaries by auto
+        have "pi / 2 \<le> ub_pi prec * Float 1 (- 1)" unfolding Float_num times_divide_eq_right mult_1_left using pi_boundaries by auto
         from order_less_le_trans[OF arctan_ubound this, THEN less_imp_le]
-        show ?thesis unfolding ub_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 -1`] if_P[OF `x \<le> Float 1 1`] if_P[OF True] .
+        show ?thesis unfolding ub_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 (- 1)`] if_P[OF `x \<le> Float 1 1`] if_P[OF True] .
       next
         case False
         hence "real ?DIV \<le> 1" by auto
@@ -638,7 +638,7 @@
           using arctan_monotone'[OF monotone] by (auto intro!: mult_left_mono)
         also have "\<dots> \<le> (Float 1 1 * ?ub_horner ?DIV)" unfolding Float_num
           using arctan_0_1_bounds[OF `0 \<le> real ?DIV` `real ?DIV \<le> 1`] by auto
-        finally show ?thesis unfolding ub_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 -1`] if_P[OF `x \<le> Float 1 1`] if_not_P[OF False] .
+        finally show ?thesis unfolding ub_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 (- 1)`] if_P[OF `x \<le> Float 1 1`] if_not_P[OF False] .
       qed
     next
       case False
@@ -661,9 +661,9 @@
         using `0 \<le> arctan x` arctan_inverse[OF `1 / x \<noteq> 0`]
         unfolding real_sgn_pos[OF `0 < 1 / x`] le_diff_eq by auto
       moreover
-      have "pi / 2 \<le> ub_pi prec * Float 1 -1" unfolding Float_num times_divide_eq_right mult_1_right using pi_boundaries by auto
+      have "pi / 2 \<le> ub_pi prec * Float 1 (- 1)" unfolding Float_num times_divide_eq_right mult_1_right using pi_boundaries by auto
       ultimately
-      show ?thesis unfolding ub_arctan.simps Let_def if_not_P[OF `\<not> x < 0`]if_not_P[OF `\<not> x \<le> Float 1 -1`] if_not_P[OF False]
+      show ?thesis unfolding ub_arctan.simps Let_def if_not_P[OF `\<not> x < 0`]if_not_P[OF `\<not> x \<le> Float 1 (- 1)`] if_not_P[OF False]
         by auto
     qed
   qed
@@ -715,8 +715,8 @@
     (lapprox_rat prec 1 k) - x * (ub_sin_cos_aux prec n (i + 2) (k * i * (i + 1)) x)"
 
 lemma cos_aux:
-  shows "(lb_sin_cos_aux prec n 1 1 (x * x)) \<le> (\<Sum> i=0..<n. -1^i * (1/real (fact (2 * i))) * x ^(2 * i))" (is "?lb")
-  and "(\<Sum> i=0..<n. -1^i * (1/real (fact (2 * i))) * x^(2 * i)) \<le> (ub_sin_cos_aux prec n 1 1 (x * x))" (is "?ub")
+  shows "(lb_sin_cos_aux prec n 1 1 (x * x)) \<le> (\<Sum> i=0..<n. (- 1) ^ i * (1/real (fact (2 * i))) * x ^(2 * i))" (is "?lb")
+  and "(\<Sum> i=0..<n. (- 1) ^ i * (1/real (fact (2 * i))) * x^(2 * i)) \<le> (ub_sin_cos_aux prec n 1 1 (x * x))" (is "?ub")
 proof -
   have "0 \<le> real (x * x)" by auto
   let "?f n" = "fact (2 * n)"
@@ -738,15 +738,15 @@
   hence "0 < x" and "0 < real x" using `0 \<le> real x` by auto
   have "0 < x * x" using `0 < x` by simp
 
-  { fix x n have "(\<Sum> i=0..<n. -1^i * (1/real (fact (2 * i))) * x ^ (2 * i))
-    = (\<Sum> i = 0 ..< 2 * n. (if even(i) then (-1 ^ (i div 2))/(real (fact i)) else 0) * x ^ i)" (is "?sum = ?ifsum")
+  { fix x n have "(\<Sum> i=0..<n. (- 1) ^ i * (1/real (fact (2 * i))) * x ^ (2 * i))
+    = (\<Sum> i = 0 ..< 2 * n. (if even(i) then ((- 1) ^ (i div 2))/(real (fact i)) else 0) * x ^ i)" (is "?sum = ?ifsum")
   proof -
     have "?sum = ?sum + (\<Sum> j = 0 ..< n. 0)" by auto
     also have "\<dots> =
-      (\<Sum> j = 0 ..< n. -1 ^ ((2 * j) div 2) / (real (fact (2 * j))) * x ^(2 * j)) + (\<Sum> j = 0 ..< n. 0)" by auto
-    also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. if even i then -1 ^ (i div 2) / (real (fact i)) * x ^ i else 0)"
+      (\<Sum> j = 0 ..< n. (- 1) ^ ((2 * j) div 2) / (real (fact (2 * j))) * x ^(2 * j)) + (\<Sum> j = 0 ..< n. 0)" by auto
+    also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. if even i then (- 1) ^ (i div 2) / (real (fact i)) * x ^ i else 0)"
       unfolding sum_split_even_odd atLeast0LessThan ..
-    also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. (if even i then -1 ^ (i div 2) / (real (fact i)) else 0) * x ^ i)"
+    also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. (if even i then (- 1) ^ (i div 2) / (real (fact i)) else 0) * x ^ i)"
       by (rule setsum.cong) auto
     finally show ?thesis by assumption
   qed } note morph_to_if_power = this
@@ -755,16 +755,16 @@
   { fix n :: nat assume "0 < n"
     hence "0 < 2 * n" by auto
     obtain t where "0 < t" and "t < real x" and
-      cos_eq: "cos x = (\<Sum> i = 0 ..< 2 * n. (if even(i) then (-1 ^ (i div 2))/(real (fact i)) else 0) * (real x) ^ i)
+      cos_eq: "cos x = (\<Sum> i = 0 ..< 2 * n. (if even(i) then ((- 1) ^ (i div 2))/(real (fact i)) else 0) * (real x) ^ i)
       + (cos (t + 1/2 * (2 * n) * pi) / real (fact (2*n))) * (real x)^(2*n)"
       (is "_ = ?SUM + ?rest / ?fact * ?pow")
       using Maclaurin_cos_expansion2[OF `0 < real x` `0 < 2 * n`]
       unfolding cos_coeff_def atLeast0LessThan by auto
 
-    have "cos t * -1^n = cos t * cos (n * pi) + sin t * sin (n * pi)" by auto
+    have "cos t * (- 1) ^ n = cos t * cos (n * pi) + sin t * sin (n * pi)" by auto
     also have "\<dots> = cos (t + n * pi)"  using cos_add by auto
     also have "\<dots> = ?rest" by auto
-    finally have "cos t * -1^n = ?rest" .
+    finally have "cos t * (- 1) ^ n = ?rest" .
     moreover
     have "t \<le> pi / 2" using `t < real x` and `x \<le> pi / 2` by auto
     hence "0 \<le> cos t" using `0 < t` and cos_ge_zero by auto
@@ -828,8 +828,8 @@
 qed
 
 lemma sin_aux: assumes "0 \<le> real x"
-  shows "(x * lb_sin_cos_aux prec n 2 1 (x * x)) \<le> (\<Sum> i=0..<n. -1^i * (1/real (fact (2 * i + 1))) * x^(2 * i + 1))" (is "?lb")
-  and "(\<Sum> i=0..<n. -1^i * (1/real (fact (2 * i + 1))) * x^(2 * i + 1)) \<le> (x * ub_sin_cos_aux prec n 2 1 (x * x))" (is "?ub")
+  shows "(x * lb_sin_cos_aux prec n 2 1 (x * x)) \<le> (\<Sum> i=0..<n. (- 1) ^ i * (1/real (fact (2 * i + 1))) * x^(2 * i + 1))" (is "?lb")
+  and "(\<Sum> i=0..<n. (- 1) ^ i * (1/real (fact (2 * i + 1))) * x^(2 * i + 1)) \<le> (x * ub_sin_cos_aux prec n 2 1 (x * x))" (is "?ub")
 proof -
   have "0 \<le> real (x * x)" by auto
   let "?f n" = "fact (2 * n + 1)"
@@ -854,14 +854,14 @@
   hence "0 < x" and "0 < real x" using `0 \<le> real x` by auto
   have "0 < x * x" using `0 < x` by simp
 
-  { fix x n have "(\<Sum> j = 0 ..< n. -1 ^ (((2 * j + 1) - Suc 0) div 2) / (real (fact (2 * j + 1))) * x ^(2 * j + 1))
-    = (\<Sum> i = 0 ..< 2 * n. (if even(i) then 0 else (-1 ^ ((i - Suc 0) div 2))/(real (fact i))) * x ^ i)" (is "?SUM = _")
+  { fix x n have "(\<Sum> j = 0 ..< n. (- 1) ^ (((2 * j + 1) - Suc 0) div 2) / (real (fact (2 * j + 1))) * x ^(2 * j + 1))
+    = (\<Sum> i = 0 ..< 2 * n. (if even(i) then 0 else ((- 1) ^ ((i - Suc 0) div 2))/(real (fact i))) * x ^ i)" (is "?SUM = _")
     proof -
       have pow: "!!i. x ^ (2 * i + 1) = x * x ^ (2 * i)" by auto
       have "?SUM = (\<Sum> j = 0 ..< n. 0) + ?SUM" by auto
-      also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. if even i then 0 else -1 ^ ((i - Suc 0) div 2) / (real (fact i)) * x ^ i)"
+      also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. if even i then 0 else (- 1) ^ ((i - Suc 0) div 2) / (real (fact i)) * x ^ i)"
         unfolding sum_split_even_odd atLeast0LessThan ..
-      also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. (if even i then 0 else -1 ^ ((i - Suc 0) div 2) / (real (fact i))) * x ^ i)"
+      also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. (if even i then 0 else (- 1) ^ ((i - Suc 0) div 2) / (real (fact i))) * x ^ i)"
         by (rule setsum.cong) auto
       finally show ?thesis by assumption
     qed } note setsum_morph = this
@@ -869,13 +869,13 @@
   { fix n :: nat assume "0 < n"
     hence "0 < 2 * n + 1" by auto
     obtain t where "0 < t" and "t < real x" and
-      sin_eq: "sin x = (\<Sum> i = 0 ..< 2 * n + 1. (if even(i) then 0 else (-1 ^ ((i - Suc 0) div 2))/(real (fact i))) * (real x) ^ i)
+      sin_eq: "sin x = (\<Sum> i = 0 ..< 2 * n + 1. (if even(i) then 0 else ((- 1) ^ ((i - Suc 0) div 2))/(real (fact i))) * (real x) ^ i)
       + (sin (t + 1/2 * (2 * n + 1) * pi) / real (fact (2*n + 1))) * (real x)^(2*n + 1)"
       (is "_ = ?SUM + ?rest / ?fact * ?pow")
       using Maclaurin_sin_expansion3[OF `0 < 2 * n + 1` `0 < real x`]
       unfolding sin_coeff_def atLeast0LessThan by auto
 
-    have "?rest = cos t * -1^n" unfolding sin_add cos_add real_of_nat_add distrib_right distrib_left by auto
+    have "?rest = cos t * (- 1) ^ n" unfolding sin_add cos_add real_of_nat_add distrib_right distrib_left by auto
     moreover
     have "t \<le> pi / 2" using `t < real x` and `x \<le> pi / 2` by auto
     hence "0 \<le> cos t" using `0 < t` and cos_ge_zero by auto
@@ -887,7 +887,7 @@
     {
       assume "even n"
       have "(x * lb_sin_cos_aux prec n 2 1 (x * x)) \<le>
-            (\<Sum> i = 0 ..< 2 * n. (if even(i) then 0 else (-1 ^ ((i - Suc 0) div 2))/(real (fact i))) * (real x) ^ i)"
+            (\<Sum> i = 0 ..< 2 * n. (if even(i) then 0 else ((- 1) ^ ((i - Suc 0) div 2))/(real (fact i))) * (real x) ^ i)"
         using sin_aux[OF `0 \<le> real x`] unfolding setsum_morph[symmetric] by auto
       also have "\<dots> \<le> ?SUM" by auto
       also have "\<dots> \<le> sin x"
@@ -908,7 +908,7 @@
           by (metis mult_nonneg_nonneg divide_nonneg_pos less_imp_le)
         thus ?thesis unfolding sin_eq by auto
       qed
-      also have "\<dots> \<le> (\<Sum> i = 0 ..< 2 * n. (if even(i) then 0 else (-1 ^ ((i - Suc 0) div 2))/(real (fact i))) * (real x) ^ i)"
+      also have "\<dots> \<le> (\<Sum> i = 0 ..< 2 * n. (if even(i) then 0 else ((- 1) ^ ((i - Suc 0) div 2))/(real (fact i))) * (real x) ^ i)"
          by auto
       also have "\<dots> \<le> (x * ub_sin_cos_aux prec n 2 1 (x * x))"
         using sin_aux[OF `0 \<le> real x`] unfolding setsum_morph[symmetric] by auto
@@ -945,17 +945,17 @@
 "lb_cos prec x = (let
     horner = \<lambda> x. lb_sin_cos_aux prec (get_even (prec div 4 + 1)) 1 1 (x * x) ;
     half = \<lambda> x. if x < 0 then - 1 else Float 1 1 * x * x - 1
-  in if x < Float 1 -1 then horner x
-else if x < 1          then half (horner (x * Float 1 -1))
-                       else half (half (horner (x * Float 1 -2))))"
+  in if x < Float 1 (- 1) then horner x
+else if x < 1          then half (horner (x * Float 1 (- 1)))
+                       else half (half (horner (x * Float 1 (- 2)))))"
 
 definition ub_cos :: "nat \<Rightarrow> float \<Rightarrow> float" where
 "ub_cos prec x = (let
     horner = \<lambda> x. ub_sin_cos_aux prec (get_odd (prec div 4 + 1)) 1 1 (x * x) ;
     half = \<lambda> x. Float 1 1 * x * x - 1
-  in if x < Float 1 -1 then horner x
-else if x < 1          then half (horner (x * Float 1 -1))
-                       else half (half (horner (x * Float 1 -2))))"
+  in if x < Float 1 (- 1) then horner x
+else if x < 1          then half (horner (x * Float 1 (- 1)))
+                       else half (half (horner (x * Float 1 (- 2)))))"
 
 lemma lb_cos: assumes "0 \<le> real x" and "x \<le> pi"
   shows "cos x \<in> {(lb_cos prec x) .. (ub_cos prec x)}" (is "?cos x \<in> {(?lb x) .. (?ub x) }")
@@ -975,13 +975,13 @@
   let "?lb_half x" = "if x < 0 then - 1 else Float 1 1 * x * x - 1"
 
   show ?thesis
-  proof (cases "x < Float 1 -1")
+  proof (cases "x < Float 1 (- 1)")
     case True hence "x \<le> pi / 2" using pi_ge_two by auto
-    show ?thesis unfolding lb_cos_def[where x=x] ub_cos_def[where x=x] if_not_P[OF `\<not> x < 0`] if_P[OF `x < Float 1 -1`] Let_def
+    show ?thesis unfolding lb_cos_def[where x=x] ub_cos_def[where x=x] if_not_P[OF `\<not> x < 0`] if_P[OF `x < Float 1 (- 1)`] Let_def
       using cos_boundaries[OF `0 \<le> real x` `x \<le> pi / 2`] .
   next
     case False
-    { fix y x :: float let ?x2 = "(x * Float 1 -1)"
+    { fix y x :: float let ?x2 = "(x * Float 1 (- 1))"
       assume "y \<le> cos ?x2" and "-pi \<le> x" and "x \<le> pi"
       hence "- (pi / 2) \<le> ?x2" and "?x2 \<le> pi / 2" using pi_ge_two unfolding Float_num by auto
       hence "0 \<le> cos ?x2" by (rule cos_ge_zero)
@@ -1000,7 +1000,7 @@
       qed
     } note lb_half = this
 
-    { fix y x :: float let ?x2 = "(x * Float 1 -1)"
+    { fix y x :: float let ?x2 = "(x * Float 1 (- 1))"
       assume ub: "cos ?x2 \<le> y" and "- pi \<le> x" and "x \<le> pi"
       hence "- (pi / 2) \<le> ?x2" and "?x2 \<le> pi / 2" using pi_ge_two unfolding Float_num by auto
       hence "0 \<le> cos ?x2" by (rule cos_ge_zero)
@@ -1016,8 +1016,8 @@
       qed
     } note ub_half = this
 
-    let ?x2 = "x * Float 1 -1"
-    let ?x4 = "x * Float 1 -1 * Float 1 -1"
+    let ?x2 = "x * Float 1 (- 1)"
+    let ?x4 = "x * Float 1 (- 1) * Float 1 (- 1)"
 
     have "-pi \<le> x" using pi_ge_zero[THEN le_imp_neg_le, unfolded minus_zero] `0 \<le> real x` by (rule order_trans)
 
@@ -1031,12 +1031,12 @@
       have "(?lb x) \<le> ?cos x"
       proof -
         from lb_half[OF lb `-pi \<le> x` `x \<le> pi`]
-        show ?thesis unfolding lb_cos_def[where x=x] Let_def using `\<not> x < 0` `\<not> x < Float 1 -1` `x < 1` by auto
+        show ?thesis unfolding lb_cos_def[where x=x] Let_def using `\<not> x < 0` `\<not> x < Float 1 (- 1)` `x < 1` by auto
       qed
       moreover have "?cos x \<le> (?ub x)"
       proof -
         from ub_half[OF ub `-pi \<le> x` `x \<le> pi`]
-        show ?thesis unfolding ub_cos_def[where x=x] Let_def using `\<not> x < 0` `\<not> x < Float 1 -1` `x < 1` by auto
+        show ?thesis unfolding ub_cos_def[where x=x] Let_def using `\<not> x < 0` `\<not> x < Float 1 (- 1)` `x < 1` by auto
       qed
       ultimately show ?thesis by auto
     next
@@ -1045,19 +1045,19 @@
       from cos_boundaries[OF this]
       have lb: "(?lb_horner ?x4) \<le> ?cos ?x4" and ub: "?cos ?x4 \<le> (?ub_horner ?x4)" by auto
 
-      have eq_4: "?x2 * Float 1 -1 = x * Float 1 -2" by transfer simp
+      have eq_4: "?x2 * Float 1 (- 1) = x * Float 1 (- 2)" by transfer simp
 
       have "(?lb x) \<le> ?cos x"
       proof -
         have "-pi \<le> ?x2" and "?x2 \<le> pi" using pi_ge_two `0 \<le> real x` `x \<le> pi` by auto
         from lb_half[OF lb_half[OF lb this] `-pi \<le> x` `x \<le> pi`, unfolded eq_4]
-        show ?thesis unfolding lb_cos_def[where x=x] if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x < Float 1 -1`] if_not_P[OF `\<not> x < 1`] Let_def .
+        show ?thesis unfolding lb_cos_def[where x=x] if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x < Float 1 (- 1)`] if_not_P[OF `\<not> x < 1`] Let_def .
       qed
       moreover have "?cos x \<le> (?ub x)"
       proof -
         have "-pi \<le> ?x2" and "?x2 \<le> pi" using pi_ge_two `0 \<le> real x` ` x \<le> pi` by auto
         from ub_half[OF ub_half[OF ub this] `-pi \<le> x` `x \<le> pi`, unfolded eq_4]
-        show ?thesis unfolding ub_cos_def[where x=x] if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x < Float 1 -1`] if_not_P[OF `\<not> x < 1`] Let_def .
+        show ?thesis unfolding ub_cos_def[where x=x] if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x < Float 1 (- 1)`] if_not_P[OF `\<not> x < 1`] Let_def .
       qed
       ultimately show ?thesis by auto
     qed
@@ -1081,9 +1081,9 @@
   in   if - lpi \<le> lx \<and> ux \<le> 0    then (lb_cos prec (-lx), ub_cos prec (-ux))
   else if 0 \<le> lx \<and> ux \<le> lpi      then (lb_cos prec ux, ub_cos prec lx)
   else if - lpi \<le> lx \<and> ux \<le> lpi  then (min (lb_cos prec (-lx)) (lb_cos prec ux), Float 1 0)
-  else if 0 \<le> lx \<and> ux \<le> 2 * lpi  then (Float -1 0, max (ub_cos prec lx) (ub_cos prec (- (ux - 2 * lpi))))
-  else if -2 * lpi \<le> lx \<and> ux \<le> 0 then (Float -1 0, max (ub_cos prec (lx + 2 * lpi)) (ub_cos prec (-ux)))
-                                 else (Float -1 0, Float 1 0))"
+  else if 0 \<le> lx \<and> ux \<le> 2 * lpi  then (Float (- 1) 0, max (ub_cos prec lx) (ub_cos prec (- (ux - 2 * lpi))))
+  else if -2 * lpi \<le> lx \<and> ux \<le> 0 then (Float (- 1) 0, max (ub_cos prec (lx + 2 * lpi)) (ub_cos prec (-ux)))
+                                 else (Float (- 1) 0, Float 1 0))"
 
 lemma floor_int:
   obtains k :: int where "real k = (floor_fl f)"
@@ -1233,7 +1233,7 @@
   next case False note 3 = this show ?thesis
   proof (cases "0 \<le> ?lx \<and> ?ux \<le> 2 * ?lpi")
     case True note Cond = this with bnds 1 2 3
-    have l: "l = Float -1 0"
+    have l: "l = Float (- 1) 0"
       and u: "u = max (ub_cos prec ?lx) (ub_cos prec (- (?ux - 2 * ?lpi)))"
       by (auto simp add: bnds_cos_def Let_def)
 
@@ -1275,7 +1275,7 @@
   next case False note 4 = this show ?thesis
   proof (cases "-2 * ?lpi \<le> ?lx \<and> ?ux \<le> 0")
     case True note Cond = this with bnds 1 2 3 4
-    have l: "l = Float -1 0"
+    have l: "l = Float (- 1) 0"
       and u: "u = max (ub_cos prec (?lx + 2 * ?lpi)) (ub_cos prec (-?ux))"
       by (auto simp add: bnds_cos_def Let_def)
 
@@ -1379,7 +1379,7 @@
 function ub_exp :: "nat \<Rightarrow> float \<Rightarrow> float" and lb_exp :: "nat \<Rightarrow> float \<Rightarrow> float" where
 "lb_exp prec x = (if 0 < x then float_divl prec 1 (ub_exp prec (-x))
              else let
-                horner = (\<lambda> x. let  y = lb_exp_horner prec (get_even (prec + 2)) 1 1 x  in if y \<le> 0 then Float 1 -2 else y)
+                horner = (\<lambda> x. let  y = lb_exp_horner prec (get_even (prec + 2)) 1 1 x  in if y \<le> 0 then Float 1 (- 2) else y)
              in if x < - 1 then (horner (float_divl prec x (- floor_fl x))) ^ nat (- int_floor_fl x)
                            else horner x)" |
 "ub_exp prec x = (if 0 < x    then float_divr prec 1 (lb_exp prec (-x))
@@ -1392,7 +1392,7 @@
 proof -
   have eq4: "4 = Suc (Suc (Suc (Suc 0)))" by auto
 
-  have "1 / 4 = (Float 1 -2)" unfolding Float_num by auto
+  have "1 / 4 = (Float 1 (- 2))" unfolding Float_num by auto
   also have "\<dots> \<le> lb_exp_horner 1 (get_even 4) 1 1 (- 1)"
     unfolding get_even_def eq4
     by (auto simp add: Float.compute_lapprox_rat Float.compute_rapprox_rat
@@ -1404,7 +1404,7 @@
 lemma lb_exp_pos: assumes "\<not> 0 < x" shows "0 < lb_exp prec x"
 proof -
   let "?lb_horner x" = "lb_exp_horner prec (get_even (prec + 2)) 1 1 x"
-  let "?horner x" = "let  y = ?lb_horner x  in if y \<le> 0 then Float 1 -2 else y"
+  let "?horner x" = "let  y = ?lb_horner x  in if y \<le> 0 then Float 1 (- 2) else y"
   have pos_horner: "\<And> x. 0 < ?horner x" unfolding Let_def by (cases "?lb_horner x \<le> 0", auto)
   moreover { fix x :: float fix num :: nat
     have "0 < real (?horner x) ^ num" using `0 < ?horner x` by simp
@@ -1431,7 +1431,7 @@
       from `\<not> x < - 1` have "- 1 \<le> real x" by auto
       hence "exp (- 1) \<le> exp x" unfolding exp_le_cancel_iff .
       from order_trans[OF exp_m1_ge_quarter this]
-      have "Float 1 -2 \<le> exp x" unfolding Float_num .
+      have "Float 1 (- 2) \<le> exp x" unfolding Float_num .
       moreover case True
       ultimately show ?thesis using bnds_exp_horner `real x \<le> 0` `\<not> x > 0` `\<not> x < - 1` by auto
     next
@@ -1502,8 +1502,8 @@
         from divide_right_mono_neg[OF floor_fl[of x] `real (floor_fl x) \<le> 0`, unfolded divide_self[OF `real (floor_fl x) \<noteq> 0`]]
         have "- 1 \<le> x / (- floor_fl x)" unfolding minus_float.rep_eq by auto
         from order_trans[OF exp_m1_ge_quarter this[unfolded exp_le_cancel_iff[where x="- 1", symmetric]]]
-        have "Float 1 -2 \<le> exp (x / (- floor_fl x))" unfolding Float_num .
-        hence "real (Float 1 -2) ^ ?num \<le> exp (x / (- floor_fl x)) ^ ?num"
+        have "Float 1 (- 2) \<le> exp (x / (- floor_fl x))" unfolding Float_num .
+        hence "real (Float 1 (- 2)) ^ ?num \<le> exp (x / (- floor_fl x)) ^ ?num"
           by (auto intro!: power_mono)
         also have "\<dots> = exp x" unfolding num_eq fl_eq exp_real_of_nat_mult[symmetric] using `real (floor_fl x) \<noteq> 0` by auto
         finally show ?thesis
@@ -1582,12 +1582,12 @@
 
 lemma ln_bounds:
   assumes "0 \<le> x" and "x < 1"
-  shows "(\<Sum>i=0..<2*n. -1^i * (1 / real (i + 1)) * x ^ (Suc i)) \<le> ln (x + 1)" (is "?lb")
-  and "ln (x + 1) \<le> (\<Sum>i=0..<2*n + 1. -1^i * (1 / real (i + 1)) * x ^ (Suc i))" (is "?ub")
+  shows "(\<Sum>i=0..<2*n. (- 1) ^ i * (1 / real (i + 1)) * x ^ (Suc i)) \<le> ln (x + 1)" (is "?lb")
+  and "ln (x + 1) \<le> (\<Sum>i=0..<2*n + 1. (- 1) ^ i * (1 / real (i + 1)) * x ^ (Suc i))" (is "?ub")
 proof -
   let "?a n" = "(1/real (n +1)) * x ^ (Suc n)"
 
-  have ln_eq: "(\<Sum> i. -1^i * ?a i) = ln (x + 1)"
+  have ln_eq: "(\<Sum> i. (- 1) ^ i * ?a i) = ln (x + 1)"
     using ln_series[of "x + 1"] `0 \<le> x` `x < 1` by auto
 
   have "norm x < 1" using assms by auto
@@ -1613,7 +1613,7 @@
   obtain ev where ev: "get_even n = 2 * ev" using get_even_double ..
   obtain od where od: "get_odd n = 2 * od + 1" using get_odd_double ..
 
-  let "?s n" = "-1^n * (1 / real (1 + n)) * (real x)^(Suc n)"
+  let "?s n" = "(- 1) ^ n * (1 / real (1 + n)) * (real x)^(Suc n)"
 
   have "?lb \<le> setsum ?s {0 ..< 2 * ev}" unfolding power_Suc2 mult.assoc[symmetric] times_float.rep_eq setsum_left_distrib[symmetric] unfolding mult.commute[of "real x"] ev
     using horner_bounds(1)[where G="\<lambda> i k. Suc k" and F="\<lambda>x. x" and f="\<lambda>x. x" and lb="\<lambda>n i k x. lb_ln_horner prec n k x" and ub="\<lambda>n i k x. ub_ln_horner prec n k x" and j'=1 and n="2*ev",
@@ -1643,10 +1643,10 @@
 subsection "Compute the logarithm of 2"
 
 definition ub_ln2 where "ub_ln2 prec = (let third = rapprox_rat (max prec 1) 1 3
-                                        in (Float 1 -1 * ub_ln_horner prec (get_odd prec) 1 (Float 1 -1)) +
+                                        in (Float 1 (- 1) * ub_ln_horner prec (get_odd prec) 1 (Float 1 (- 1))) +
                                            (third * ub_ln_horner prec (get_odd prec) 1 third))"
 definition lb_ln2 where "lb_ln2 prec = (let third = lapprox_rat prec 1 3
-                                        in (Float 1 -1 * lb_ln_horner prec (get_even prec) 1 (Float 1 -1)) +
+                                        in (Float 1 (- 1) * lb_ln_horner prec (get_even prec) 1 (Float 1 (- 1))) +
                                            (third * lb_ln_horner prec (get_even prec) 1 third))"
 
 lemma ub_ln2: "ln 2 \<le> ub_ln2 prec" (is "?ub_ln2")
@@ -1663,7 +1663,7 @@
   have ub3: "1 / 3 \<le> ?uthird" using rapprox_rat[of 1 3] by auto
   hence ub3_lb: "0 \<le> real ?uthird" by auto
 
-  have lb2: "0 \<le> real (Float 1 -1)" and ub2: "real (Float 1 -1) < 1" unfolding Float_num by auto
+  have lb2: "0 \<le> real (Float 1 (- 1))" and ub2: "real (Float 1 (- 1)) < 1" unfolding Float_num by auto
 
   have "0 \<le> (1::int)" and "0 < (3::int)" by auto
   have ub3_ub: "real ?uthird < 1" by (simp add: Float.compute_rapprox_rat rapprox_posrat_less1)
@@ -1694,15 +1694,15 @@
 "ub_ln prec x = (if x \<le> 0          then None
             else if x < 1          then Some (- the (lb_ln prec (float_divl (max prec 1) 1 x)))
             else let horner = \<lambda>x. x * ub_ln_horner prec (get_odd prec) 1 x in
-                 if x \<le> Float 3 -1 then Some (horner (x - 1))
-            else if x < Float 1 1  then Some (horner (Float 1 -1) + horner (x * rapprox_rat prec 2 3 - 1))
+                 if x \<le> Float 3 (- 1) then Some (horner (x - 1))
+            else if x < Float 1 1  then Some (horner (Float 1 (- 1)) + horner (x * rapprox_rat prec 2 3 - 1))
                                    else let l = bitlen (mantissa x) - 1 in
                                         Some (ub_ln2 prec * (Float (exponent x + l) 0) + horner (Float (mantissa x) (- l) - 1)))" |
 "lb_ln prec x = (if x \<le> 0          then None
             else if x < 1          then Some (- the (ub_ln prec (float_divr prec 1 x)))
             else let horner = \<lambda>x. x * lb_ln_horner prec (get_even prec) 1 x in
-                 if x \<le> Float 3 -1 then Some (horner (x - 1))
-            else if x < Float 1 1  then Some (horner (Float 1 -1) +
+                 if x \<le> Float 3 (- 1) then Some (horner (x - 1))
+            else if x < Float 1 1  then Some (horner (Float 1 (- 1)) +
                                               horner (max (x * lapprox_rat prec 2 3 - 1) 0))
                                    else let l = bitlen (mantissa x) - 1 in
                                         Some (lb_ln2 prec * (Float (exponent x + l) 0) + horner (Float (mantissa x) (- l) - 1)))"
@@ -1761,16 +1761,16 @@
   shows "ub_ln prec x = (if x \<le> 0          then None
               else if x < 1          then Some (- the (lb_ln prec (float_divl (max prec 1) 1 x)))
             else let horner = \<lambda>x. x * ub_ln_horner prec (get_odd prec) 1 x in
-                 if x \<le> Float 3 -1 then Some (horner (x - 1))
-            else if x < Float 1 1  then Some (horner (Float 1 -1) + horner (x * rapprox_rat prec 2 3 - 1))
+                 if x \<le> Float 3 (- 1) then Some (horner (x - 1))
+            else if x < Float 1 1  then Some (horner (Float 1 (- 1)) + horner (x * rapprox_rat prec 2 3 - 1))
                                    else let l = bitlen m - 1 in
                                         Some (ub_ln2 prec * (Float (e + l) 0) + horner (Float m (- l) - 1)))"
     (is ?th1)
   and "lb_ln prec x = (if x \<le> 0          then None
             else if x < 1          then Some (- the (ub_ln prec (float_divr prec 1 x)))
             else let horner = \<lambda>x. x * lb_ln_horner prec (get_even prec) 1 x in
-                 if x \<le> Float 3 -1 then Some (horner (x - 1))
-            else if x < Float 1 1  then Some (horner (Float 1 -1) +
+                 if x \<le> Float 3 (- 1) then Some (horner (x - 1))
+            else if x < Float 1 1  then Some (horner (Float 1 (- 1)) +
                                               horner (max (x * lapprox_rat prec 2 3 - 1) 0))
                                    else let l = bitlen m - 1 in
                                         Some (lb_ln2 prec * (Float (e + l) 0) + horner (Float m (- l) - 1)))"
@@ -1816,10 +1816,10 @@
   have "\<not> x \<le> 0" and "\<not> x < 1" using `1 \<le> x` by auto
   hence "0 \<le> real (x - 1)" using `1 \<le> x` by auto
 
-  have [simp]: "(Float 3 -1) = 3 / 2" by simp
+  have [simp]: "(Float 3 (- 1)) = 3 / 2" by simp
 
   show ?thesis
-  proof (cases "x \<le> Float 3 -1")
+  proof (cases "x \<le> Float 3 (- 1)")
     case True
     show ?thesis unfolding lb_ln.simps unfolding ub_ln.simps Let_def
       using ln_float_bounds[OF `0 \<le> real (x - 1)` `real (x - 1) < 1`, of prec] `\<not> x \<le> 0` `\<not> x < 1` True
@@ -1856,9 +1856,9 @@
         show "0 \<le> real (x * rapprox_rat prec 2 3 - 1)" using pos by auto
       qed
       finally have "ln x
-        \<le> ?ub_horner (Float 1 -1)
+        \<le> ?ub_horner (Float 1 (- 1))
           + ?ub_horner (x * rapprox_rat prec 2 3 - 1)"
-        using ln_float_bounds(2)[of "Float 1 -1" prec prec] add by auto }
+        using ln_float_bounds(2)[of "Float 1 (- 1)" prec prec] add by auto }
     moreover
     { let ?max = "max (x * lapprox_rat prec 2 3 - 1) 0"
 
@@ -1884,16 +1884,16 @@
           by (cases "0 < real x * real (lapprox_posrat prec 2 3) - 1",
               auto simp add: max_def)
       qed
-      finally have "?lb_horner (Float 1 -1) + ?lb_horner ?max
+      finally have "?lb_horner (Float 1 (- 1)) + ?lb_horner ?max
         \<le> ln x"
-        using ln_float_bounds(1)[of "Float 1 -1" prec prec] add by auto }
+        using ln_float_bounds(1)[of "Float 1 (- 1)" prec prec] add by auto }
     ultimately
     show ?thesis unfolding lb_ln.simps unfolding ub_ln.simps Let_def
       using `\<not> x \<le> 0` `\<not> x < 1` True False by auto
   qed
 next
   case False
-  hence "\<not> x \<le> 0" and "\<not> x < 1" "0 < x" "\<not> x \<le> Float 3 -1"
+  hence "\<not> x \<le> 0" and "\<not> x < 1" "0 < x" "\<not> x \<le> Float 3 (- 1)"
     using `1 \<le> x` by auto
   show ?thesis
   proof -
@@ -1946,7 +1946,7 @@
         unfolding Float ln_shifted_float[OF `0 < m`, of e] by auto
     }
     ultimately show ?thesis unfolding lb_ln.simps unfolding ub_ln.simps
-      unfolding if_not_P[OF `\<not> x \<le> 0`] if_not_P[OF `\<not> x < 1`] if_not_P[OF False] if_not_P[OF `\<not> x \<le> Float 3 -1`] Let_def
+      unfolding if_not_P[OF `\<not> x \<le> 0`] if_not_P[OF `\<not> x < 1`] if_not_P[OF False] if_not_P[OF `\<not> x \<le> Float 3 (- 1)`] Let_def
       unfolding plus_float.rep_eq e_def[symmetric] m_def[symmetric] by simp
   qed
 qed
@@ -2079,14 +2079,14 @@
 lemma interpret_floatarith_diff: "interpret_floatarith (Add a (Minus b)) vs = (interpret_floatarith a vs) - (interpret_floatarith b vs)"
   unfolding interpret_floatarith.simps by simp
 
-lemma interpret_floatarith_sin: "interpret_floatarith (Cos (Add (Mult Pi (Num (Float 1 -1))) (Minus a))) vs =
+lemma interpret_floatarith_sin: "interpret_floatarith (Cos (Add (Mult Pi (Num (Float 1 (- 1)))) (Minus a))) vs =
   sin (interpret_floatarith a vs)"
   unfolding sin_cos_eq interpret_floatarith.simps
             interpret_floatarith_divide interpret_floatarith_diff
   by auto
 
 lemma interpret_floatarith_tan:
-  "interpret_floatarith (Mult (Cos (Add (Mult Pi (Num (Float 1 -1))) (Minus a))) (Inverse (Cos a))) vs =
+  "interpret_floatarith (Mult (Cos (Add (Mult Pi (Num (Float 1 (- 1)))) (Minus a))) (Inverse (Cos a))) vs =
    tan (interpret_floatarith a vs)"
   unfolding interpret_floatarith.simps(3,4) interpret_floatarith_sin tan_def divide_inverse
   by auto
@@ -2472,7 +2472,7 @@
 fun approx_form' and approx_form :: "nat \<Rightarrow> form \<Rightarrow> (float * float) option list \<Rightarrow> nat list \<Rightarrow> bool" where
 "approx_form' prec f 0 n l u bs ss = approx_form prec f (bs[n := Some (l, u)]) ss" |
 "approx_form' prec f (Suc s) n l u bs ss =
-  (let m = (l + u) * Float 1 -1
+  (let m = (l + u) * Float 1 (- 1)
    in (if approx_form' prec f s n l m bs ss then approx_form' prec f s n m u bs ss else False))" |
 "approx_form prec (Bound (Var n) a b f) bs ss =
    (case (approx prec a bs, approx prec b bs)
@@ -2509,7 +2509,7 @@
 next
   case (Suc s)
 
-  let ?m = "(l + u) * Float 1 -1"
+  let ?m = "(l + u) * Float 1 (- 1)"
   have "real l \<le> ?m" and "?m \<le> real u"
     unfolding less_eq_float_def using Suc.prems by auto
 
@@ -2644,7 +2644,7 @@
 "DERIV_floatarith x (Mult a b)        = Add (Mult a (DERIV_floatarith x b)) (Mult (DERIV_floatarith x a) b)" |
 "DERIV_floatarith x (Minus a)         = Minus (DERIV_floatarith x a)" |
 "DERIV_floatarith x (Inverse a)       = Minus (Mult (DERIV_floatarith x a) (Inverse (Power a 2)))" |
-"DERIV_floatarith x (Cos a)           = Minus (Mult (Cos (Add (Mult Pi (Num (Float 1 -1))) (Minus a))) (DERIV_floatarith x a))" |
+"DERIV_floatarith x (Cos a)           = Minus (Mult (Cos (Add (Mult Pi (Num (Float 1 (- 1)))) (Minus a))) (DERIV_floatarith x a))" |
 "DERIV_floatarith x (Arctan a)        = Mult (Inverse (Add (Num 1) (Power a 2))) (DERIV_floatarith x a)" |
 "DERIV_floatarith x (Min a b)         = Num 0" |
 "DERIV_floatarith x (Max a b)         = Num 0" |
@@ -3040,10 +3040,10 @@
 
 fun approx_tse_form' where
 "approx_tse_form' prec t f 0 l u cmp =
-  (case approx_tse prec 0 t ((l + u) * Float 1 -1) 1 f [Some (l, u)]
+  (case approx_tse prec 0 t ((l + u) * Float 1 (- 1)) 1 f [Some (l, u)]
      of Some (l, u) \<Rightarrow> cmp l u | None \<Rightarrow> False)" |
 "approx_tse_form' prec t f (Suc s) l u cmp =
-  (let m = (l + u) * Float 1 -1
+  (let m = (l + u) * Float 1 (- 1)
    in (if approx_tse_form' prec t f s l m cmp then
       approx_tse_form' prec t f s m u cmp else False))"
 
@@ -3051,16 +3051,16 @@
   fixes x :: real
   assumes "approx_tse_form' prec t f s l u cmp" and "x \<in> {l .. u}"
   shows "\<exists> l' u' ly uy. x \<in> { l' .. u' } \<and> real l \<le> l' \<and> u' \<le> real u \<and> cmp ly uy \<and>
-                  approx_tse prec 0 t ((l' + u') * Float 1 -1) 1 f [Some (l', u')] = Some (ly, uy)"
+                  approx_tse prec 0 t ((l' + u') * Float 1 (- 1)) 1 f [Some (l', u')] = Some (ly, uy)"
 using assms proof (induct s arbitrary: l u)
   case 0
   then obtain ly uy
-    where *: "approx_tse prec 0 t ((l + u) * Float 1 -1) 1 f [Some (l, u)] = Some (ly, uy)"
+    where *: "approx_tse prec 0 t ((l + u) * Float 1 (- 1)) 1 f [Some (l, u)] = Some (ly, uy)"
     and **: "cmp ly uy" by (auto elim!: case_optionE)
   with 0 show ?case by auto
 next
   case (Suc s)
-  let ?m = "(l + u) * Float 1 -1"
+  let ?m = "(l + u) * Float 1 (- 1)"
   from Suc.prems
   have l: "approx_tse_form' prec t f s l ?m cmp"
     and u: "approx_tse_form' prec t f s ?m u cmp"
@@ -3077,14 +3077,14 @@
     from Suc.hyps[OF l this]
     obtain l' u' ly uy
       where "x \<in> { l' .. u' } \<and> real l \<le> l' \<and> real u' \<le> ?m \<and> cmp ly uy \<and>
-                  approx_tse prec 0 t ((l' + u') * Float 1 -1) 1 f [Some (l', u')] = Some (ly, uy)" by blast
+                  approx_tse prec 0 t ((l' + u') * Float 1 (- 1)) 1 f [Some (l', u')] = Some (ly, uy)" by blast
     with m_u show ?thesis by (auto intro!: exI)
   next
     assume "x \<in> { ?m .. u }"
     from Suc.hyps[OF u this]
     obtain l' u' ly uy
       where "x \<in> { l' .. u' } \<and> ?m \<le> real l' \<and> u' \<le> real u \<and> cmp ly uy \<and>
-                  approx_tse prec 0 t ((l' + u') * Float 1 -1) 1 f [Some (l', u')] = Some (ly, uy)" by blast
+                  approx_tse prec 0 t ((l' + u') * Float 1 (- 1)) 1 f [Some (l', u')] = Some (ly, uy)" by blast
     with m_u show ?thesis by (auto intro!: exI)
   qed
 qed
@@ -3099,7 +3099,7 @@
   obtain l' u' ly uy
     where x': "x \<in> { l' .. u' }" and "l \<le> real l'"
     and "real u' \<le> u" and "0 < ly"
-    and tse: "approx_tse prec 0 t ((l' + u') * Float 1 -1) 1 (Add a (Minus b)) [Some (l', u')] = Some (ly, uy)"
+    and tse: "approx_tse prec 0 t ((l' + u') * Float 1 (- 1)) 1 (Add a (Minus b)) [Some (l', u')] = Some (ly, uy)"
     by blast
 
   hence "bounded_by [x] [Some (l', u')]" by (auto simp add: bounded_by_def)
@@ -3121,7 +3121,7 @@
   obtain l' u' ly uy
     where x': "x \<in> { l' .. u' }" and "l \<le> real l'"
     and "real u' \<le> u" and "0 \<le> ly"
-    and tse: "approx_tse prec 0 t ((l' + u') * Float 1 -1) 1 (Add a (Minus b)) [Some (l', u')] = Some (ly, uy)"
+    and tse: "approx_tse prec 0 t ((l' + u') * Float 1 (- 1)) 1 (Add a (Minus b)) [Some (l', u')] = Some (ly, uy)"
     by blast
 
   hence "bounded_by [x] [Some (l', u')]" by (auto simp add: bounded_by_def)
diff -r 24096e89c131 -r 6d46ad54a2ab src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy	Sun Sep 21 16:56:11 2014 +0200
@@ -1458,22 +1458,22 @@
 recdef \<beta> "measure size"
   "\<beta> (And p q) = (\<beta> p @ \<beta> q)"
   "\<beta> (Or p q) = (\<beta> p @ \<beta> q)"
-  "\<beta> (Eq  (CN 0 c e)) = [Sub (C -1) e]"
+  "\<beta> (Eq  (CN 0 c e)) = [Sub (C (- 1)) e]"
   "\<beta> (NEq (CN 0 c e)) = [Neg e]"
   "\<beta> (Lt  (CN 0 c e)) = []"
   "\<beta> (Le  (CN 0 c e)) = []"
   "\<beta> (Gt  (CN 0 c e)) = [Neg e]"
-  "\<beta> (Ge  (CN 0 c e)) = [Sub (C -1) e]"
+  "\<beta> (Ge  (CN 0 c e)) = [Sub (C (- 1)) e]"
   "\<beta> p = []"
 
 consts \<alpha> :: "fm \<Rightarrow> num list"
 recdef \<alpha> "measure size"
   "\<alpha> (And p q) = \<alpha> p @ \<alpha> q"
   "\<alpha> (Or p q) = \<alpha> p @ \<alpha> q"
-  "\<alpha> (Eq  (CN 0 c e)) = [Add (C -1) e]"
+  "\<alpha> (Eq  (CN 0 c e)) = [Add (C (- 1)) e]"
   "\<alpha> (NEq (CN 0 c e)) = [e]"
   "\<alpha> (Lt  (CN 0 c e)) = [e]"
-  "\<alpha> (Le  (CN 0 c e)) = [Add (C -1) e]"
+  "\<alpha> (Le  (CN 0 c e)) = [Add (C (- 1)) e]"
   "\<alpha> (Gt  (CN 0 c e)) = []"
   "\<alpha> (Ge  (CN 0 c e)) = []"
   "\<alpha> p = []"
@@ -2082,7 +2082,7 @@
   moreover
   {
     assume H: "\<not> (x - d) + ?e \<ge> 0"
-    let ?v = "Sub (C -1) e"
+    let ?v = "Sub (C (- 1)) e"
     have vb: "?v \<in> set (\<beta> (Ge (CN 0 c e)))"
       by simp
     from 8(5)[simplified simp_thms Inum.simps \<beta>.simps list.set bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]]
@@ -2109,7 +2109,7 @@
     and bn: "numbound0 e"
     by simp_all
   let ?e = "Inum (x # bs) e"
-  let ?v="(Sub (C -1) e)"
+  let ?v="(Sub (C (- 1)) e)"
   have vb: "?v \<in> set (\<beta> (Eq (CN 0 c e)))"
     by simp
   from p have "x= - ?e"
diff -r 24096e89c131 -r 6d46ad54a2ab src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy	Sun Sep 21 16:56:11 2014 +0200
@@ -2304,21 +2304,21 @@
 recdef \<beta> "measure size"
   "\<beta> (And p q) = (\<beta> p @ \<beta> q)" 
   "\<beta> (Or p q) = (\<beta> p @ \<beta> q)" 
-  "\<beta> (Eq  (CN 0 c e)) = [Sub (C -1) e]"
+  "\<beta> (Eq  (CN 0 c e)) = [Sub (C (- 1)) e]"
   "\<beta> (NEq (CN 0 c e)) = [Neg e]"
   "\<beta> (Lt  (CN 0 c e)) = []"
   "\<beta> (Le  (CN 0 c e)) = []"
   "\<beta> (Gt  (CN 0 c e)) = [Neg e]"
-  "\<beta> (Ge  (CN 0 c e)) = [Sub (C -1) e]"
+  "\<beta> (Ge  (CN 0 c e)) = [Sub (C (- 1)) e]"
   "\<beta> p = []"
 
 recdef \<alpha> "measure size"
   "\<alpha> (And p q) = (\<alpha> p @ \<alpha> q)" 
   "\<alpha> (Or p q) = (\<alpha> p @ \<alpha> q)" 
-  "\<alpha> (Eq  (CN 0 c e)) = [Add (C -1) e]"
+  "\<alpha> (Eq  (CN 0 c e)) = [Add (C (- 1)) e]"
   "\<alpha> (NEq (CN 0 c e)) = [e]"
   "\<alpha> (Lt  (CN 0 c e)) = [e]"
-  "\<alpha> (Le  (CN 0 c e)) = [Add (C -1) e]"
+  "\<alpha> (Le  (CN 0 c e)) = [Add (C (- 1)) e]"
   "\<alpha> (Gt  (CN 0 c e)) = []"
   "\<alpha> (Ge  (CN 0 c e)) = []"
   "\<alpha> p = []"
@@ -2636,7 +2636,7 @@
         by (simp del: real_of_int_minus)}
     moreover
     {assume H: "\<not> real (x-d) + ?e \<ge> 0" 
-      let ?v="Sub (C -1) e"
+      let ?v="Sub (C (- 1)) e"
       have vb: "?v \<in> set (\<beta> (Ge (CN 0 c e)))" by simp
       from 8(5)[simplified simp_thms Inum.simps \<beta>.simps list.set bex_simps numbound0_I[OF bn,where b="a" and b'="real x" and bs="bs"]] 
       have nob: "\<not> (\<exists> j\<in> {1 ..d}. real x =  - ?e - 1 + real j)" by auto 
@@ -2656,7 +2656,7 @@
   case (3 c e) hence p: "Ifm (real x #bs) (Eq (CN 0 c e))" (is "?p x") and c1: "c=1" 
     and bn:"numbound0 e" and ie1: "isint e (a #bs)" using dvd1_eq1[where x="c"] by simp+
     let ?e = "Inum (real x # bs) e"
-    let ?v="(Sub (C -1) e)"
+    let ?v="(Sub (C (- 1)) e)"
     have vb: "?v \<in> set (\<beta> (Eq (CN 0 c e)))" by simp
     from p have "real x= - ?e" by (simp add: c1) with 3(5) show ?case using dp
       by simp (erule ballE[where x="1"],
@@ -2796,7 +2796,7 @@
 recdef \<rho> "measure size"
   "\<rho> (And p q) = (\<rho> p @ \<rho> q)" 
   "\<rho> (Or p q) = (\<rho> p @ \<rho> q)" 
-  "\<rho> (Eq  (CN 0 c e)) = [(Sub (C -1) e,c)]"
+  "\<rho> (Eq  (CN 0 c e)) = [(Sub (C (- 1)) e,c)]"
   "\<rho> (NEq (CN 0 c e)) = [(Neg e,c)]"
   "\<rho> (Lt  (CN 0 c e)) = []"
   "\<rho> (Le  (CN 0 c e)) = []"
@@ -2828,10 +2828,10 @@
 recdef \<alpha>_\<rho> "measure size"
   "\<alpha>_\<rho> (And p q) = (\<alpha>_\<rho> p @ \<alpha>_\<rho> q)" 
   "\<alpha>_\<rho> (Or p q) = (\<alpha>_\<rho> p @ \<alpha>_\<rho> q)" 
-  "\<alpha>_\<rho> (Eq  (CN 0 c e)) = [(Add (C -1) e,c)]"
+  "\<alpha>_\<rho> (Eq  (CN 0 c e)) = [(Add (C (- 1)) e,c)]"
   "\<alpha>_\<rho> (NEq (CN 0 c e)) = [(e,c)]"
   "\<alpha>_\<rho> (Lt  (CN 0 c e)) = [(e,c)]"
-  "\<alpha>_\<rho> (Le  (CN 0 c e)) = [(Add (C -1) e,c)]"
+  "\<alpha>_\<rho> (Le  (CN 0 c e)) = [(Add (C (- 1)) e,c)]"
   "\<alpha>_\<rho> p = []"
 
     (* Simulates normal substituion by modifying the formula see correctness theorem *)
@@ -4856,9 +4856,9 @@
   let ?P = "?I x (plusinf ?rq)"
   have MF: "?M = False"
     apply (simp add: Let_def reducecoeff_def numgcd_def rsplit_def ge_def lt_def conj_def disj_def)
-    by (cases "rlfm p = And (Ge (CN 0 1 (C 0))) (Lt (CN 0 1 (C -1)))", simp_all)
+    by (cases "rlfm p = And (Ge (CN 0 1 (C 0))) (Lt (CN 0 1 (C (- 1))))", simp_all)
   have PF: "?P = False" apply (simp add: Let_def reducecoeff_def numgcd_def rsplit_def ge_def lt_def conj_def disj_def)
-    by (cases "rlfm p = And (Ge (CN 0 1 (C 0))) (Lt (CN 0 1 (C -1)))", simp_all)
+    by (cases "rlfm p = And (Ge (CN 0 1 (C 0))) (Lt (CN 0 1 (C (- 1))))", simp_all)
   have "(\<exists> x. ?I x ?q ) = 
     ((?I x (minusinf ?rq)) \<or> (?I x (plusinf ?rq )) \<or> (\<exists> (t,n) \<in> set (\<Upsilon> ?rq). \<exists> (s,m) \<in> set (\<Upsilon> ?rq ). ?I x (\<upsilon> ?rq (Add (Mul m t) (Mul n s), 2*n*m))))"
     (is "(\<exists> x. ?I x ?q) = (?M \<or> ?P \<or> ?F)" is "?E = ?D")
diff -r 24096e89c131 -r 6d46ad54a2ab src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Divides.thy	Sun Sep 21 16:56:11 2014 +0200
@@ -1664,7 +1664,7 @@
 lemma posDivAlg_0_right [simp]: "posDivAlg a 0 = (0, a)"
 by (subst posDivAlg.simps, auto)
 
-lemma negDivAlg_minus1 [simp]: "negDivAlg -1 b = (-1, b - 1)"
+lemma negDivAlg_minus1 [simp]: "negDivAlg (- 1) b = (- 1, b - 1)"
 by (subst negDivAlg.simps, auto)
 
 lemma divmod_int_rel_neg: "divmod_int_rel (-a) (-b) qr ==> divmod_int_rel a b (apsnd uminus qr)"
diff -r 24096e89c131 -r 6d46ad54a2ab src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy	Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy	Sun Sep 21 16:56:11 2014 +0200
@@ -252,7 +252,7 @@
 definition "test3_ivl =
  ''x'' ::= N 0;; ''y'' ::= N 100;; ''z'' ::= Plus (V ''x'') (V ''y'');;
  WHILE Less (V ''x'') (N 11)
- DO (''x'' ::= Plus (V ''x'') (N 1);; ''y'' ::= Plus (V ''y'') (N -1))"
+ DO (''x'' ::= Plus (V ''x'') (N 1);; ''y'' ::= Plus (V ''y'') (N (- 1)))"
 value "list_up(AI_ivl test3_ivl Top)"
 
 definition "test4_ivl =
@@ -264,7 +264,7 @@
 text{* Nontermination not detected: *}
 definition "test5_ivl =
  ''x'' ::= N 0;;
- WHILE Less (V ''x'') (N 1) DO ''x'' ::= Plus (V ''x'') (N -1)"
+ WHILE Less (V ''x'') (N 1) DO ''x'' ::= Plus (V ''x'') (N (- 1))"
 value "list_up(AI_ivl test5_ivl Top)"
 
 end
diff -r 24096e89c131 -r 6d46ad54a2ab src/HOL/IMP/Abs_Int_Tests.thy
--- a/src/HOL/IMP/Abs_Int_Tests.thy	Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/IMP/Abs_Int_Tests.thy	Sun Sep 21 16:56:11 2014 +0200
@@ -63,6 +63,6 @@
 
 definition "test6_ivl =
  ''x'' ::= N 0;;
- WHILE Less (N -1) (V ''x'') DO ''x'' ::= Plus (V ''x'') (N 1)"
+ WHILE Less (N (- 1)) (V ''x'') DO ''x'' ::= Plus (V ''x'') (N 1)"
 
 end
diff -r 24096e89c131 -r 6d46ad54a2ab src/HOL/IMP/Hoare_Examples.thy
--- a/src/HOL/IMP/Hoare_Examples.thy	Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/IMP/Hoare_Examples.thy	Sun Sep 21 16:56:11 2014 +0200
@@ -17,7 +17,7 @@
 abbreviation "wsum ==
   WHILE Less (N 0) (V ''x'')
   DO (''y'' ::= Plus (V ''y'') (V ''x'');;
-      ''x'' ::= Plus (V ''x'') (N -1))"
+      ''x'' ::= Plus (V ''x'') (N (- 1)))"
 
 
 subsubsection{* Proof by Operational Semantics *}
diff -r 24096e89c131 -r 6d46ad54a2ab src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Library/Float.thy	Sun Sep 21 16:56:11 2014 +0200
@@ -205,7 +205,7 @@
     done
   assume "a < b"
   then show "\<exists>c. a < c \<and> c < b"
-    apply (intro exI[of _ "(a + b) * Float 1 -1"])
+    apply (intro exI[of _ "(a + b) * Float 1 (- 1)"])
     apply transfer
     apply (simp add: powr_minus)
     done
@@ -1085,8 +1085,8 @@
 
 lemma Float_num[simp]: shows
    "real (Float 1 0) = 1" and "real (Float 1 1) = 2" and "real (Float 1 2) = 4" and
-   "real (Float 1 -1) = 1/2" and "real (Float 1 -2) = 1/4" and "real (Float 1 -3) = 1/8" and
-   "real (Float -1 0) = -1" and "real (Float (number_of n) 0) = number_of n"
+   "real (Float 1 (- 1)) = 1/2" and "real (Float 1 (- 2)) = 1/4" and "real (Float 1 (- 3)) = 1/8" and
+   "real (Float (- 1) 0) = -1" and "real (Float (number_of n) 0) = number_of n"
 using two_powr_int_float[of 2] two_powr_int_float[of "-1"] two_powr_int_float[of "-2"] two_powr_int_float[of "-3"]
 using powr_realpow[of 2 2] powr_realpow[of 2 3]
 using powr_minus[of 2 1] powr_minus[of 2 2] powr_minus[of 2 3]
diff -r 24096e89c131 -r 6d46ad54a2ab src/HOL/MacLaurin.thy
--- a/src/HOL/MacLaurin.thy	Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/MacLaurin.thy	Sun Sep 21 16:56:11 2014 +0200
@@ -221,10 +221,10 @@
     by (intro Maclaurin) (auto intro!: derivative_eq_intros DERIV')
   then guess t ..
   moreover
-  have "-1 ^ n * diff n (- t) * (- h) ^ n / real (fact n) = diff n (- t) * h ^ n / real (fact n)"
+  have "(- 1) ^ n * diff n (- t) * (- h) ^ n / real (fact n) = diff n (- t) * h ^ n / real (fact n)"
     by (auto simp add: power_mult_distrib[symmetric])
   moreover
-  have "(SUM m<n. -1 ^ m * diff m 0 * (- h) ^ m / real (fact m)) = (SUM m<n. diff m 0 * h ^ m / real (fact m))"
+  have "(SUM m<n. (- 1) ^ m * diff m 0 * (- h) ^ m / real (fact m)) = (SUM m<n. diff m 0 * h ^ m / real (fact m))"
     by (auto intro: setsum.cong simp add: power_mult_distrib[symmetric])
   ultimately have " h < - t \<and>
     - t < 0 \<and>
@@ -561,7 +561,7 @@
       ?diff n t / real (fact n) * x ^ n" by fast
   have diff_m_0:
     "\<And>m. ?diff m 0 = (if even m then 0
-         else -1 ^ ((m - Suc 0) div 2))"
+         else (- 1) ^ ((m - Suc 0) div 2))"
     apply (subst even_even_mod_4_iff)
     apply (cut_tac m=m in mod_exhaust_less_4)
     apply (elim disjE, simp_all)
diff -r 24096e89c131 -r 6d46ad54a2ab src/HOL/Multivariate_Analysis/Fashoda.thy
--- a/src/HOL/Multivariate_Analysis/Fashoda.thy	Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Fashoda.thy	Sun Sep 21 16:56:11 2014 +0200
@@ -146,7 +146,7 @@
     using UNIV_2 by auto
   have 1: "box (- 1) (1::real^2) \<noteq> {}"
     unfolding interval_eq_empty_cart by auto
-  have 2: "continuous_on (cbox -1 1) (negatex \<circ> sqprojection \<circ> ?F)"
+  have 2: "continuous_on (cbox (- 1) 1) (negatex \<circ> sqprojection \<circ> ?F)"
     apply (intro continuous_intros continuous_on_component)
     unfolding *
     apply (rule assms)+
@@ -179,7 +179,7 @@
   proof -
     case goal1
     then obtain y :: "real^2" where y:
-        "y \<in> cbox -1 1"
+        "y \<in> cbox (- 1) 1"
         "x = (negatex \<circ> sqprojection \<circ> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w)) y"
       unfolding image_iff ..
     have "?F y \<noteq> 0"
@@ -208,9 +208,9 @@
     qed
   qed
   obtain x :: "real^2" where x:
-      "x \<in> cbox -1 1"
+      "x \<in> cbox (- 1) 1"
       "(negatex \<circ> sqprojection \<circ> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w)) x = x"
-    apply (rule brouwer_weak[of "cbox -1 (1::real^2)" "negatex \<circ> sqprojection \<circ> ?F"])
+    apply (rule brouwer_weak[of "cbox (- 1) (1::real^2)" "negatex \<circ> sqprojection \<circ> ?F"])
     apply (rule compact_cbox convex_box)+
     unfolding interior_cbox
     apply (rule 1 2 3)+
@@ -362,7 +362,7 @@
     unfolding iscale_def by auto
   have "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. (f \<circ> iscale) s = (g \<circ> iscale) t"
   proof (rule fashoda_unit)
-    show "(f \<circ> iscale) ` {- 1..1} \<subseteq> cbox -1 1" "(g \<circ> iscale) ` {- 1..1} \<subseteq> cbox -1 1"
+    show "(f \<circ> iscale) ` {- 1..1} \<subseteq> cbox (- 1) 1" "(g \<circ> iscale) ` {- 1..1} \<subseteq> cbox (- 1) 1"
       using isc and assms(3-4) by (auto simp add: image_comp [symmetric])
     have *: "continuous_on {- 1..1} iscale"
       unfolding iscale_def by (rule continuous_intros)+
@@ -506,7 +506,7 @@
         "y \<in> {0..1}"
         "x = (interval_bij (a, b) (- 1, 1) \<circ> f) y"
       unfolding image_iff ..
-    show "x \<in> cbox -1 1"
+    show "x \<in> cbox (- 1) 1"
       unfolding y o_def
       apply (rule in_interval_interval_bij)
       using y(1)
@@ -520,7 +520,7 @@
         "y \<in> {0..1}"
         "x = (interval_bij (a, b) (- 1, 1) \<circ> g) y"
       unfolding image_iff ..
-    show "x \<in> cbox -1 1"
+    show "x \<in> cbox (- 1) 1"
       unfolding y o_def
       apply (rule in_interval_interval_bij)
       using y(1)
diff -r 24096e89c131 -r 6d46ad54a2ab src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Sun Sep 21 16:56:11 2014 +0200
@@ -11000,7 +11000,7 @@
   shows "g integrable_on s \<and> ((\<lambda>k. integral s (f k)) ---> integral s g) sequentially"
 proof -
   note assm = assms[rule_format]
-  have *: "{integral s (\<lambda>x. - f k x) |k. True} = op *\<^sub>R -1 ` {integral s (f k)| k. True}"
+  have *: "{integral s (\<lambda>x. - f k x) |k. True} = op *\<^sub>R (- 1) ` {integral s (f k)| k. True}"
     apply safe
     unfolding image_iff
     apply (rule_tac x="integral s (f k)" in bexI)
diff -r 24096e89c131 -r 6d46ad54a2ab src/HOL/NSA/HyperDef.thy
--- a/src/HOL/NSA/HyperDef.thy	Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/NSA/HyperDef.thy	Sun Sep 21 16:56:11 2014 +0200
@@ -523,7 +523,7 @@
 done
 
 lemma hyperpow_minus_one2 [simp]:
-     "\<And>n. -1 pow (2*n) = (1::hypreal)"
+     "\<And>n. (- 1) pow (2*n) = (1::hypreal)"
 by transfer (rule power_minus1_even)
 
 lemma hyperpow_less_le:
diff -r 24096e89c131 -r 6d46ad54a2ab src/HOL/Num.thy
--- a/src/HOL/Num.thy	Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Num.thy	Sun Sep 21 16:56:11 2014 +0200
@@ -280,31 +280,14 @@
 syntax
   "_Numeral" :: "num_const \<Rightarrow> 'a"    ("_")
 
+ML_file "Tools/numeral.ML"
+
 parse_translation {*
   let
-    fun num_of_int n =
-      if n > 0 then
-        (case IntInf.quotRem (n, 2) of
-          (0, 1) => Syntax.const @{const_syntax One}
-        | (n, 0) => Syntax.const @{const_syntax Bit0} $ num_of_int n
-        | (n, 1) => Syntax.const @{const_syntax Bit1} $ num_of_int n)
-      else raise Match
-    val numeral = Syntax.const @{const_syntax numeral}
-    val uminus = Syntax.const @{const_syntax uminus}
-    val one = Syntax.const @{const_syntax Groups.one}
-    val zero = Syntax.const @{const_syntax Groups.zero}
     fun numeral_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
           c $ numeral_tr [t] $ u
       | numeral_tr [Const (num, _)] =
-          let
-            val {value, ...} = Lexicon.read_xnum num;
-          in
-            if value = 0 then zero else
-            if value > 0
-            then numeral $ num_of_int value
-            else if value = ~1 then uminus $ one
-            else uminus $ (numeral $ num_of_int (~ value))
-          end
+          (Numeral.mk_number_syntax o #value o Lexicon.read_xnum) num
       | numeral_tr ts = raise TERM ("numeral_tr", ts);
   in [(@{syntax_const "_Numeral"}, K numeral_tr)] end
 *}
@@ -334,8 +317,6 @@
   end
 *}
 
-ML_file "Tools/numeral.ML"
-
 
 subsection {* Class-specific numeral rules *}
 
diff -r 24096e89c131 -r 6d46ad54a2ab src/HOL/Number_Theory/Binomial.thy
--- a/src/HOL/Number_Theory/Binomial.thy	Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Number_Theory/Binomial.thy	Sun Sep 21 16:56:11 2014 +0200
@@ -695,19 +695,19 @@
 
 lemma card_UNION:
   assumes "finite A" and "\<forall>k \<in> A. finite k"
-  shows "card (\<Union>A) = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. -1 ^ (card I + 1) * int (card (\<Inter>I)))"
+  shows "card (\<Union>A) = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (- 1) ^ (card I + 1) * int (card (\<Inter>I)))"
   (is "?lhs = ?rhs")
 proof -
-  have "?rhs = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. -1 ^ (card I + 1) * (\<Sum>_\<in>\<Inter>I. 1))" by simp
-  also have "\<dots> = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (\<Sum>_\<in>\<Inter>I. -1 ^ (card I + 1)))" (is "_ = nat ?rhs")
+  have "?rhs = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (- 1) ^ (card I + 1) * (\<Sum>_\<in>\<Inter>I. 1))" by simp
+  also have "\<dots> = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (\<Sum>_\<in>\<Inter>I. (- 1) ^ (card I + 1)))" (is "_ = nat ?rhs")
     by(subst setsum_right_distrib) simp
-  also have "?rhs = (\<Sum>(I, _)\<in>Sigma {I. I \<subseteq> A \<and> I \<noteq> {}} Inter. -1 ^ (card I + 1))"
+  also have "?rhs = (\<Sum>(I, _)\<in>Sigma {I. I \<subseteq> A \<and> I \<noteq> {}} Inter. (- 1) ^ (card I + 1))"
     using assms by(subst setsum.Sigma)(auto)
-  also have "\<dots> = (\<Sum>(x, I)\<in>(SIGMA x:UNIV. {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}). -1 ^ (card I + 1))"
+  also have "\<dots> = (\<Sum>(x, I)\<in>(SIGMA x:UNIV. {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}). (- 1) ^ (card I + 1))"
     by (rule setsum.reindex_cong [where l = "\<lambda>(x, y). (y, x)"]) (auto intro: inj_onI simp add: split_beta)
-  also have "\<dots> = (\<Sum>(x, I)\<in>(SIGMA x:\<Union>A. {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}). -1 ^ (card I + 1))"
+  also have "\<dots> = (\<Sum>(x, I)\<in>(SIGMA x:\<Union>A. {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}). (- 1) ^ (card I + 1))"
     using assms by(auto intro!: setsum.mono_neutral_cong_right finite_SigmaI2 intro: finite_subset[where B="\<Union>A"])
-  also have "\<dots> = (\<Sum>x\<in>\<Union>A. (\<Sum>I|I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I. -1 ^ (card I + 1)))" 
+  also have "\<dots> = (\<Sum>x\<in>\<Union>A. (\<Sum>I|I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I. (- 1) ^ (card I + 1)))" 
     using assms by(subst setsum.Sigma) auto
   also have "\<dots> = (\<Sum>_\<in>\<Union>A. 1)" (is "setsum ?lhs _ = _")
   proof(rule setsum.cong[OF refl])
@@ -722,13 +722,13 @@
       using assms by(auto intro!: rev_image_eqI[where x="(card a, a)" for a]
         simp add: card_gt_0_iff[folded Suc_le_eq]
         dest: finite_subset intro: card_mono)
-    ultimately have "?lhs x = (\<Sum>(i, I)\<in>(SIGMA i:{1..card A}. ?I i). -1 ^ (i + 1))"
+    ultimately have "?lhs x = (\<Sum>(i, I)\<in>(SIGMA i:{1..card A}. ?I i). (- 1) ^ (i + 1))"
       by (rule setsum.reindex_cong [where l = snd]) fastforce
-    also have "\<dots> = (\<Sum>i=1..card A. (\<Sum>I|I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. -1 ^ (i + 1)))"
+    also have "\<dots> = (\<Sum>i=1..card A. (\<Sum>I|I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. (- 1) ^ (i + 1)))"
       using assms by(subst setsum.Sigma) auto
-    also have "\<dots> = (\<Sum>i=1..card A. -1 ^ (i + 1) * (\<Sum>I|I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1))"
+    also have "\<dots> = (\<Sum>i=1..card A. (- 1) ^ (i + 1) * (\<Sum>I|I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1))"
       by(subst setsum_right_distrib) simp
-    also have "\<dots> = (\<Sum>i=1..card K. -1 ^ (i + 1) * (\<Sum>I|I \<subseteq> K \<and> card I = i. 1))" (is "_ = ?rhs")
+    also have "\<dots> = (\<Sum>i=1..card K. (- 1) ^ (i + 1) * (\<Sum>I|I \<subseteq> K \<and> card I = i. 1))" (is "_ = ?rhs")
     proof(rule setsum.mono_neutral_cong_right[rule_format])
       show "{1..card K} \<subseteq> {1..card A}" using `finite A`
         by(auto simp add: K_def intro: card_mono)
@@ -740,22 +740,22 @@
         by(auto simp add: K_def)
       also have "\<dots> = {}" using `finite A` i
         by(auto simp add: K_def dest: card_mono[rotated 1])
-      finally show "-1 ^ (i + 1) * (\<Sum>I | I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1 :: int) = 0"
+      finally show "(- 1) ^ (i + 1) * (\<Sum>I | I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1 :: int) = 0"
         by(simp only:) simp
     next
       fix i
       have "(\<Sum>I | I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1) = (\<Sum>I | I \<subseteq> K \<and> card I = i. 1 :: int)"
         (is "?lhs = ?rhs")
         by(rule setsum.cong)(auto simp add: K_def)
-      thus "-1 ^ (i + 1) * ?lhs = -1 ^ (i + 1) * ?rhs" by simp
+      thus "(- 1) ^ (i + 1) * ?lhs = (- 1) ^ (i + 1) * ?rhs" by simp
     qed simp
     also have "{I. I \<subseteq> K \<and> card I = 0} = {{}}" using assms
       by(auto simp add: card_eq_0_iff K_def dest: finite_subset)
-    hence "?rhs = (\<Sum>i = 0..card K. -1 ^ (i + 1) * (\<Sum>I | I \<subseteq> K \<and> card I = i. 1 :: int)) + 1"
+    hence "?rhs = (\<Sum>i = 0..card K. (- 1) ^ (i + 1) * (\<Sum>I | I \<subseteq> K \<and> card I = i. 1 :: int)) + 1"
       by(subst (2) setsum_head_Suc)(simp_all )
-    also have "\<dots> = (\<Sum>i = 0..card K. -1 * (-1 ^ i * int (card K choose i))) + 1"
+    also have "\<dots> = (\<Sum>i = 0..card K. (- 1) * ((- 1) ^ i * int (card K choose i))) + 1"
       using K by(subst n_subsets[symmetric]) simp_all
-    also have "\<dots> = - (\<Sum>i = 0..card K. -1 ^ i * int (card K choose i)) + 1"
+    also have "\<dots> = - (\<Sum>i = 0..card K. (- 1) ^ i * int (card K choose i)) + 1"
       by(subst setsum_right_distrib[symmetric]) simp
     also have "\<dots> =  - ((-1 + 1) ^ card K) + 1"
       by(subst binomial_ring)(simp add: ac_simps)
diff -r 24096e89c131 -r 6d46ad54a2ab src/HOL/Number_Theory/Gauss.thy
--- a/src/HOL/Number_Theory/Gauss.thy	Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Number_Theory/Gauss.thy	Sun Sep 21 16:56:11 2014 +0200
@@ -318,7 +318,7 @@
 
 subsection {* Gauss' Lemma *}
 
-lemma aux: "setprod id A * -1 ^ card E * a ^ card A * -1 ^ card E = setprod id A * a ^ card A"
+lemma aux: "setprod id A * (- 1) ^ card E * a ^ card A * (- 1) ^ card E = setprod id A * a ^ card A"
 by (metis (no_types) minus_minus mult.commute mult.left_commute power_minus power_one)
 
 theorem pre_gauss_lemma:
@@ -363,7 +363,7 @@
     apply (rule cong_trans_int)
     apply (simp add: aux cong del:setprod.cong)
     done
-  with A_prod_relprime have "[-1 ^ card E = a ^ card A](mod p)"
+  with A_prod_relprime have "[(- 1) ^ card E = a ^ card A](mod p)"
     by (metis cong_mult_lcancel_int)
   then show ?thesis
     by (simp add: A_card_eq cong_sym_int)
diff -r 24096e89c131 -r 6d46ad54a2ab src/HOL/Old_Number_Theory/EvenOdd.thy
--- a/src/HOL/Old_Number_Theory/EvenOdd.thy	Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Old_Number_Theory/EvenOdd.thy	Sun Sep 21 16:56:11 2014 +0200
@@ -240,8 +240,8 @@
 (* Powers of -1 and parity *)
 
 lemma neg_one_special: "finite A ==>
-    ((-1 :: int) ^ card A) * (-1 ^ card A) = 1"
-  by (induct set: finite) auto
+  ((- 1) ^ card A) * ((- 1) ^ card A) = (1 :: int)"
+  unfolding power_add [symmetric] by simp
 
 lemma neg_one_power: "(-1::int)^n = 1 | (-1::int)^n = -1"
   by (induct n) auto
diff -r 24096e89c131 -r 6d46ad54a2ab src/HOL/Old_Number_Theory/Gauss.thy
--- a/src/HOL/Old_Number_Theory/Gauss.thy	Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Old_Number_Theory/Gauss.thy	Sun Sep 21 16:56:11 2014 +0200
@@ -436,7 +436,7 @@
 
 subsection {* Gauss' Lemma *}
 
-lemma aux: "setprod id A * -1 ^ card E * a ^ card A * -1 ^ card E = setprod id A * a ^ card A"
+lemma aux: "setprod id A * (- 1) ^ card E * a ^ card A * (- 1) ^ card E = setprod id A * a ^ card A"
   by (auto simp add: finite_E neg_one_special)
 
 theorem pre_gauss_lemma:
@@ -488,8 +488,8 @@
     apply (rule zcong_trans)
     apply (simp add: aux cong del:setprod.cong)
     done
-  with this zcong_cancel2 [of p "setprod id A" "-1 ^ card E" "a ^ card A"]
-      p_g_0 A_prod_relprime have "[-1 ^ card E = a ^ card A](mod p)"
+  with this zcong_cancel2 [of p "setprod id A" "(- 1) ^ card E" "a ^ card A"]
+      p_g_0 A_prod_relprime have "[(- 1) ^ card E = a ^ card A](mod p)"
     by (simp add: order_less_imp_le)
   from this show ?thesis
     by (simp add: A_card_eq zcong_sym)
diff -r 24096e89c131 -r 6d46ad54a2ab src/HOL/Power.thy
--- a/src/HOL/Power.thy	Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Power.thy	Sun Sep 21 16:56:11 2014 +0200
@@ -214,7 +214,7 @@
   by (rule power_minus_Bit0)
 
 lemma power_minus1_even [simp]:
-  "-1 ^ (2*n) = 1"
+  "(- 1) ^ (2*n) = 1"
 proof (induct n)
   case 0 show ?case by simp
 next
@@ -222,7 +222,7 @@
 qed
 
 lemma power_minus1_odd:
-  "-1 ^ Suc (2*n) = -1"
+  "(- 1) ^ Suc (2*n) = -1"
   by simp
 
 lemma power_minus_even [simp]:
diff -r 24096e89c131 -r 6d46ad54a2ab src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Rat.thy	Sun Sep 21 16:56:11 2014 +0200
@@ -1151,29 +1151,13 @@
 
 parse_translation {*
   let
-    fun mk_number i =
-      let
-        fun mk 1 = Syntax.const @{const_syntax Num.One}
-          | mk i =
-              let
-                val (q, r) = Integer.div_mod i 2;
-                val bit = if r = 0 then @{const_syntax Num.Bit0} else @{const_syntax Num.Bit1};
-              in Syntax.const bit $ (mk q) end;
-      in
-        if i = 0 then Syntax.const @{const_syntax Groups.zero}
-        else if i > 0 then Syntax.const @{const_syntax Num.numeral} $ mk i
-        else
-          Syntax.const @{const_syntax Groups.uminus} $
-            (Syntax.const @{const_syntax Num.numeral} $ mk (~ i))
-      end;
-
     fun mk_frac str =
       let
         val {mant = i, exp = n} = Lexicon.read_float str;
         val exp = Syntax.const @{const_syntax Power.power};
-        val ten = mk_number 10;
-        val exp10 = if n = 1 then ten else exp $ ten $ mk_number n;
-      in Syntax.const @{const_syntax divide} $ mk_number i $ exp10 end;
+        val ten = Numeral.mk_number_syntax 10;
+        val exp10 = if n = 1 then ten else exp $ ten $ Numeral.mk_number_syntax n;;
+      in Syntax.const @{const_syntax divide} $ Numeral.mk_number_syntax i $ exp10 end;
 
     fun float_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = c $ float_tr [t] $ u
       | float_tr [t as Const (str, _)] = mk_frac str
diff -r 24096e89c131 -r 6d46ad54a2ab src/HOL/SMT_Examples/SMT_Word_Examples.thy
--- a/src/HOL/SMT_Examples/SMT_Word_Examples.thy	Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/SMT_Examples/SMT_Word_Examples.thy	Sun Sep 21 16:56:11 2014 +0200
@@ -27,7 +27,7 @@
 lemma "27 + 11 = (6::5 word)" by smt
 lemma "7 * 3 = (21::8 word)" by smt
 lemma "11 - 27 = (-16::8 word)" by smt
-lemma "- -11 = (11::5 word)" by smt
+lemma "- (- 11) = (11::5 word)" by smt
 lemma "-40 + 1 = (-39::7 word)" by smt
 lemma "a + 2 * b + c - b = (b + c) + (a :: 32 word)" by smt
 lemma "x = (5 :: 4 word) \<Longrightarrow> 4 * x = 4" by smt
diff -r 24096e89c131 -r 6d46ad54a2ab src/HOL/Tools/numeral.ML
--- a/src/HOL/Tools/numeral.ML	Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Tools/numeral.ML	Sun Sep 21 16:56:11 2014 +0200
@@ -8,6 +8,7 @@
 sig
   val mk_cnumeral: int -> cterm
   val mk_cnumber: ctyp -> int -> cterm
+  val mk_number_syntax: int -> term
   val add_code: string -> (int -> int) -> (Code_Printer.literals -> int -> string) -> string -> theory -> theory
 end;
 
@@ -60,6 +61,19 @@
 
 end;
 
+fun mk_num_syntax n =
+  if n > 0 then
+    (case IntInf.quotRem (n, 2) of
+      (0, 1) => Syntax.const @{const_syntax One}
+    | (n, 0) => Syntax.const @{const_syntax Bit0} $ mk_num_syntax n
+    | (n, 1) => Syntax.const @{const_syntax Bit1} $ mk_num_syntax n)
+  else raise Match
+
+fun mk_number_syntax n =
+  if n = 0 then Syntax.const @{const_syntax Groups.zero}
+  else if n = 1 then Syntax.const @{const_syntax Groups.one}
+  else Syntax.const @{const_syntax numeral} $ mk_num_syntax n;
+
 
 (* code generator *)
 
diff -r 24096e89c131 -r 6d46ad54a2ab src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Transcendental.thy	Sun Sep 21 16:56:11 2014 +0200
@@ -247,8 +247,8 @@
 lemma sums_alternating_upper_lower:
   fixes a :: "nat \<Rightarrow> real"
   assumes mono: "\<And>n. a (Suc n) \<le> a n" and a_pos: "\<And>n. 0 \<le> a n" and "a ----> 0"
-  shows "\<exists>l. ((\<forall>n. (\<Sum>i<2*n. -1^i*a i) \<le> l) \<and> (\<lambda> n. \<Sum>i<2*n. -1^i*a i) ----> l) \<and>
-             ((\<forall>n. l \<le> (\<Sum>i<2*n + 1. -1^i*a i)) \<and> (\<lambda> n. \<Sum>i<2*n + 1. -1^i*a i) ----> l)"
+  shows "\<exists>l. ((\<forall>n. (\<Sum>i<2*n. (- 1)^i*a i) \<le> l) \<and> (\<lambda> n. \<Sum>i<2*n. (- 1)^i*a i) ----> l) \<and>
+             ((\<forall>n. l \<le> (\<Sum>i<2*n + 1. (- 1)^i*a i)) \<and> (\<lambda> n. \<Sum>i<2*n + 1. (- 1)^i*a i) ----> l)"
   (is "\<exists>l. ((\<forall>n. ?f n \<le> l) \<and> _) \<and> ((\<forall>n. l \<le> ?g n) \<and> _)")
 proof (rule nested_sequence_unique)
   have fg_diff: "\<And>n. ?f n - ?g n = - a (2 * n)" unfolding One_nat_def by auto
@@ -367,11 +367,11 @@
   assumes a_zero: "a ----> 0" and "monoseq a"
   shows "summable (\<lambda> n. (-1)^n * a n)" (is "?summable")
     and "0 < a 0 \<longrightarrow>
-      (\<forall>n. (\<Sum>i. -1^i*a i) \<in> { \<Sum>i<2*n. -1^i * a i .. \<Sum>i<2*n+1. -1^i * a i})" (is "?pos")
+      (\<forall>n. (\<Sum>i. (- 1)^i*a i) \<in> { \<Sum>i<2*n. (- 1)^i * a i .. \<Sum>i<2*n+1. (- 1)^i * a i})" (is "?pos")
     and "a 0 < 0 \<longrightarrow>
-      (\<forall>n. (\<Sum>i. -1^i*a i) \<in> { \<Sum>i<2*n+1. -1^i * a i .. \<Sum>i<2*n. -1^i * a i})" (is "?neg")
-    and "(\<lambda>n. \<Sum>i<2*n. -1^i*a i) ----> (\<Sum>i. -1^i*a i)" (is "?f")
-    and "(\<lambda>n. \<Sum>i<2*n+1. -1^i*a i) ----> (\<Sum>i. -1^i*a i)" (is "?g")
+      (\<forall>n. (\<Sum>i. (- 1)^i*a i) \<in> { \<Sum>i<2*n+1. (- 1)^i * a i .. \<Sum>i<2*n. (- 1)^i * a i})" (is "?neg")
+    and "(\<lambda>n. \<Sum>i<2*n. (- 1)^i*a i) ----> (\<Sum>i. (- 1)^i*a i)" (is "?f")
+    and "(\<lambda>n. \<Sum>i<2*n+1. (- 1)^i*a i) ----> (\<Sum>i. (- 1)^i*a i)" (is "?g")
 proof -
   have "?summable \<and> ?pos \<and> ?neg \<and> ?f \<and> ?g"
   proof (cases "(\<forall> n. 0 \<le> a n) \<and> (\<forall>m. \<forall>n\<ge>m. a n \<le> a m)")
@@ -413,7 +413,7 @@
       unfolding minus_diff_minus by auto
 
     from suminf_minus[OF leibniz(1), unfolded mult_minus_right minus_minus]
-    have move_minus: "(\<Sum>n. - (-1 ^ n * a n)) = - (\<Sum>n. -1 ^ n * a n)"
+    have move_minus: "(\<Sum>n. - ((- 1) ^ n * a n)) = - (\<Sum>n. (- 1) ^ n * a n)"
       by auto
 
     have ?pos using `0 \<le> ?a 0` by auto
@@ -1383,7 +1383,7 @@
       fix x :: real
       assume "x \<in> {- 1<..<1}"
       hence "norm (-x) < 1" by auto
-      show "summable (\<lambda>n. -1 ^ n * (1 / real (n + 1)) * real (Suc n) * x ^ n)"
+      show "summable (\<lambda>n. (- 1) ^ n * (1 / real (n + 1)) * real (Suc n) * x ^ n)"
         unfolding One_nat_def
         by (auto simp add: power_mult_distrib[symmetric] summable_geometric[OF `norm (-x) < 1`])
     qed
@@ -2216,10 +2216,10 @@
 subsection {* Sine and Cosine *}
 
 definition sin_coeff :: "nat \<Rightarrow> real" where
-  "sin_coeff = (\<lambda>n. if even n then 0 else -1 ^ ((n - Suc 0) div 2) / real (fact n))"
+  "sin_coeff = (\<lambda>n. if even n then 0 else (- 1) ^ ((n - Suc 0) div 2) / real (fact n))"
 
 definition cos_coeff :: "nat \<Rightarrow> real" where
-  "cos_coeff = (\<lambda>n. if even n then (-1 ^ (n div 2)) / real (fact n) else 0)"
+  "cos_coeff = (\<lambda>n. if even n then ((- 1) ^ (n div 2)) / real (fact n) else 0)"
 
 definition sin :: "real \<Rightarrow> real"
   where "sin = (\<lambda>x. \<Sum>n. sin_coeff n * x ^ n)"
@@ -2472,7 +2472,7 @@
    hence define pi.*}
 
 lemma sin_paired:
-  "(\<lambda>n. -1 ^ n /(real (fact (2 * n + 1))) * x ^ (2 * n + 1)) sums  sin x"
+  "(\<lambda>n. (- 1) ^ n /(real (fact (2 * n + 1))) * x ^ (2 * n + 1)) sums  sin x"
 proof -
   have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. sin_coeff k * x ^ k) sums sin x"
     by (rule sin_converges [THEN sums_group], simp)
@@ -2483,7 +2483,7 @@
   assumes "0 < x" and "x < 2"
   shows "0 < sin x"
 proof -
-  let ?f = "\<lambda>n. \<Sum>k = n*2..<n*2+2. -1 ^ k / real (fact (2*k+1)) * x^(2*k+1)"
+  let ?f = "\<lambda>n. \<Sum>k = n*2..<n*2+2. (- 1) ^ k / real (fact (2*k+1)) * x^(2*k+1)"
   have pos: "\<forall>n. 0 < ?f n"
   proof
     fix n :: nat
@@ -2508,7 +2508,7 @@
 lemma cos_double_less_one: "0 < x \<Longrightarrow> x < 2 \<Longrightarrow> cos (2 * x) < 1"
   using sin_gt_zero [where x = x] by (auto simp add: cos_squared_eq cos_double)
 
-lemma cos_paired: "(\<lambda>n. -1 ^ n /(real (fact (2 * n))) * x ^ (2 * n)) sums cos x"
+lemma cos_paired: "(\<lambda>n. (- 1) ^ n /(real (fact (2 * n))) * x ^ (2 * n)) sums cos x"
 proof -
   have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. cos_coeff k * x ^ k) sums cos x"
     by (rule cos_converges [THEN sums_group], simp)
@@ -2541,16 +2541,16 @@
 proof -
   note fact_Suc [simp del]
   from cos_paired
-  have "(\<lambda>n. - (-1 ^ n / real (fact (2 * n)) * 2 ^ (2 * n))) sums - cos 2"
+  have "(\<lambda>n. - ((- 1) ^ n / real (fact (2 * n)) * 2 ^ (2 * n))) sums - cos 2"
     by (rule sums_minus)
-  then have *: "(\<lambda>n. - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n)))) sums - cos 2"
+  then have *: "(\<lambda>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n)))) sums - cos 2"
     by simp
-  then have **: "summable (\<lambda>n. - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
+  then have **: "summable (\<lambda>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
     by (rule sums_summable)
-  have "0 < (\<Sum>n<Suc (Suc (Suc 0)). - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
+  have "0 < (\<Sum>n<Suc (Suc (Suc 0)). - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
     by (simp add: fact_num_eq_if_nat realpow_num_eq_if)
-  moreover have "(\<Sum>n<Suc (Suc (Suc 0)). - (-1 ^ n  * 2 ^ (2 * n) / real (fact (2 * n))))
-    < (\<Sum>n. - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
+  moreover have "(\<Sum>n<Suc (Suc (Suc 0)). - ((- 1) ^ n  * 2 ^ (2 * n) / real (fact (2 * n))))
+    < (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
   proof -
     { fix d
       have "4 * real (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))
@@ -2569,9 +2569,9 @@
     from ** show ?thesis by (rule sumr_pos_lt_pair)
       (simp add: divide_inverse mult.assoc [symmetric] ***)
   qed
-  ultimately have "0 < (\<Sum>n. - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
+  ultimately have "0 < (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
     by (rule order_less_trans)
-  moreover from * have "- cos 2 = (\<Sum>n. - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
+  moreover from * have "- cos 2 = (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
     by (rule sums_unique)
   ultimately have "0 < - cos 2" by simp
   then show ?thesis by simp
@@ -2677,10 +2677,10 @@
 lemma cos_periodic [simp]: "cos (x + 2*pi) = cos x"
   by (simp add: cos_add cos_double)
 
-lemma cos_npi [simp]: "cos (real n * pi) = -1 ^ n"
+lemma cos_npi [simp]: "cos (real n * pi) = (- 1) ^ n"
   by (induct n) (auto simp add: real_of_nat_Suc distrib_right)
 
-lemma cos_npi2 [simp]: "cos (pi * real n) = -1 ^ n"
+lemma cos_npi2 [simp]: "cos (pi * real n) = (- 1) ^ n"
   by (metis cos_npi mult.commute)
 
 lemma sin_npi [simp]: "sin (real (n::nat) * pi) = 0"
@@ -3754,9 +3754,9 @@
     fix x :: real
     assume "\<bar>x\<bar> < 1"
     hence "x\<^sup>2 < 1" by (rule less_one_imp_sqr_less_one)
-    have "summable (\<lambda> n. -1 ^ n * (x\<^sup>2) ^n)"
+    have "summable (\<lambda> n. (- 1) ^ n * (x\<^sup>2) ^n)"
       by (rule summable_Leibniz(1), auto intro!: LIMSEQ_realpow_zero monoseq_realpow `x\<^sup>2 < 1` order_less_imp_le[OF `x\<^sup>2 < 1`])
-    hence "summable (\<lambda> n. -1 ^ n * x^(2*n))" unfolding power_mult .
+    hence "summable (\<lambda> n. (- 1) ^ n * x^(2*n))" unfolding power_mult .
   } note summable_Integral = this
 
   {
@@ -3778,17 +3778,17 @@
   } note sums_even = this
 
   have Int_eq: "(\<Sum>n. ?f n * real (Suc n) * x^n) = ?Int"
-    unfolding if_eq mult.commute[of _ 2] suminf_def sums_even[of "\<lambda> n. -1 ^ n * x ^ (2 * n)", symmetric]
+    unfolding if_eq mult.commute[of _ 2] suminf_def sums_even[of "\<lambda> n. (- 1) ^ n * x ^ (2 * n)", symmetric]
     by auto
 
   {
     fix x :: real
-    have if_eq': "\<And>n. (if even n then -1 ^ (n div 2) * 1 / real (Suc n) else 0) * x ^ Suc n =
-      (if even n then -1 ^ (n div 2) * (1 / real (Suc (2 * (n div 2))) * x ^ Suc (2 * (n div 2))) else 0)"
+    have if_eq': "\<And>n. (if even n then (- 1) ^ (n div 2) * 1 / real (Suc n) else 0) * x ^ Suc n =
+      (if even n then (- 1) ^ (n div 2) * (1 / real (Suc (2 * (n div 2))) * x ^ Suc (2 * (n div 2))) else 0)"
       using n_even by auto
     have idx_eq: "\<And>n. n * 2 + 1 = Suc (2 * n)" by auto
     have "(\<Sum>n. ?f n * x^(Suc n)) = ?arctan x"
-      unfolding if_eq' idx_eq suminf_def sums_even[of "\<lambda> n. -1 ^ n * (1 / real (Suc (2 * n)) * x ^ Suc (2 * n))", symmetric]
+      unfolding if_eq' idx_eq suminf_def sums_even[of "\<lambda> n. (- 1) ^ n * (1 / real (Suc (2 * n)) * x ^ Suc (2 * n))", symmetric]
       by auto
   } note arctan_eq = this
 
@@ -3798,11 +3798,18 @@
     {
       fix x' :: real
       assume x'_bounds: "x' \<in> {- 1 <..< 1}"
-      hence "\<bar>x'\<bar> < 1" by auto
-
+      then have "\<bar>x'\<bar> < 1" by auto
+      then
+        have *: "summable (\<lambda>n. (- 1) ^ n * x' ^ (2 * n))"
+        by (rule summable_Integral)
       let ?S = "\<Sum> n. (-1)^n * x'^(2 * n)"
       show "summable (\<lambda> n. ?f n * real (Suc n) * x'^n)" unfolding if_eq
-        by (rule sums_summable[where l="0 + ?S"], rule sums_if, rule sums_zero, rule summable_sums, rule summable_Integral[OF `\<bar>x'\<bar> < 1`])
+        apply (rule sums_summable [where l="0 + ?S"])
+        apply (rule sums_if)
+        apply (rule sums_zero)
+        apply (rule summable_sums)
+        apply (rule *)
+        done
     }
   qed auto
   thus ?thesis unfolding Int_eq arctan_eq .
diff -r 24096e89c131 -r 6d46ad54a2ab src/HOL/Word/Bit_Representation.thy
--- a/src/HOL/Word/Bit_Representation.thy	Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Word/Bit_Representation.thy	Sun Sep 21 16:56:11 2014 +0200
@@ -98,7 +98,7 @@
 lemma bin_last_numeral_simps [simp]:
   "\<not> bin_last 0"
   "bin_last 1"
-  "bin_last -1"
+  "bin_last (- 1)"
   "bin_last Numeral1"
   "\<not> bin_last (numeral (Num.Bit0 w))"
   "bin_last (numeral (Num.Bit1 w))"
@@ -109,7 +109,7 @@
 lemma bin_rest_numeral_simps [simp]:
   "bin_rest 0 = 0"
   "bin_rest 1 = 0"
-  "bin_rest -1 = -1"
+  "bin_rest (- 1) = - 1"
   "bin_rest Numeral1 = 0"
   "bin_rest (numeral (Num.Bit0 w)) = numeral w"
   "bin_rest (numeral (Num.Bit1 w)) = numeral w"
@@ -182,7 +182,7 @@
 
 lemma bin_induct:
   assumes PPls: "P 0"
-    and PMin: "P -1"
+    and PMin: "P (- 1)"
     and PBit: "!!bin bit. P bin ==> P (bin BIT bit)"
   shows "P bin"
   apply (rule_tac P=P and a=bin and f1="nat o abs" 
@@ -242,7 +242,7 @@
 lemma bin_nth_1 [simp]: "bin_nth 1 n \<longleftrightarrow> n = 0"
   by (cases n) simp_all
 
-lemma bin_nth_minus1 [simp]: "bin_nth -1 n"
+lemma bin_nth_minus1 [simp]: "bin_nth (- 1) n"
   by (induct n) auto
 
 lemma bin_nth_0_BIT: "bin_nth (w BIT b) 0 \<longleftrightarrow> b"
@@ -328,12 +328,12 @@
 lemma sbintrunc_n_0 [simp]: "sbintrunc n 0 = 0"
   by (induct n) auto
 
-lemma sbintrunc_n_minus1 [simp]: "sbintrunc n -1 = -1"
+lemma sbintrunc_n_minus1 [simp]: "sbintrunc n (- 1) = -1"
   by (induct n) auto
 
 lemma bintrunc_Suc_numeral:
   "bintrunc (Suc n) 1 = 1"
-  "bintrunc (Suc n) -1 = bintrunc n -1 BIT True"
+  "bintrunc (Suc n) (- 1) = bintrunc n (- 1) BIT True"
   "bintrunc (Suc n) (numeral (Num.Bit0 w)) = bintrunc n (numeral w) BIT False"
   "bintrunc (Suc n) (numeral (Num.Bit1 w)) = bintrunc n (numeral w) BIT True"
   "bintrunc (Suc n) (- numeral (Num.Bit0 w)) =
@@ -678,7 +678,7 @@
 lemma bintr_lt2p: "bintrunc n w < 2 ^ n"
   by (simp add: bintrunc_mod2p)
 
-lemma bintr_Min: "bintrunc n -1 = 2 ^ n - 1"
+lemma bintr_Min: "bintrunc n (- 1) = 2 ^ n - 1"
   by (simp add: bintrunc_mod2p m1mod2k)
 
 lemma sbintr_ge: "- (2 ^ n) \<le> sbintrunc n w"
diff -r 24096e89c131 -r 6d46ad54a2ab src/HOL/Word/Bits_Int.thy
--- a/src/HOL/Word/Bits_Int.thy	Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Word/Bits_Int.thy	Sun Sep 21 16:56:11 2014 +0200
@@ -462,7 +462,7 @@
 lemma bin_sc_FP [simp]: "bin_sc n False 0 = 0"
   by (induct n) auto
 
-lemma bin_sc_TM [simp]: "bin_sc n True -1 = -1"
+lemma bin_sc_TM [simp]: "bin_sc n True (- 1) = - 1"
   by (induct n) auto
   
 lemmas bin_sc_simps = bin_sc.Z bin_sc.Suc bin_sc_TM bin_sc_FP
@@ -583,7 +583,7 @@
   by (induct n) auto
 
 lemma bin_split_minus1 [simp]:
-  "bin_split n -1 = (-1, bintrunc n -1)"
+  "bin_split n (- 1) = (- 1, bintrunc n (- 1))"
   by (induct n) auto
 
 lemma bin_split_trunc:
diff -r 24096e89c131 -r 6d46ad54a2ab src/HOL/Word/Bool_List_Representation.thy
--- a/src/HOL/Word/Bool_List_Representation.thy	Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Word/Bool_List_Representation.thy	Sun Sep 21 16:56:11 2014 +0200
@@ -105,8 +105,8 @@
   by (cases n) auto
 
 lemma bin_to_bl_aux_minus1_minus_simp [simp]:
-  "0 < n ==> bin_to_bl_aux n -1 bl = 
-    bin_to_bl_aux (n - 1) -1 (True # bl)"
+  "0 < n ==> bin_to_bl_aux n (- 1) bl = 
+    bin_to_bl_aux (n - 1) (- 1) (True # bl)"
   by (cases n) auto
 
 lemma bin_to_bl_aux_one_minus_simp [simp]:
@@ -206,10 +206,10 @@
   unfolding bin_to_bl_def by (simp add: bin_to_bl_zero_aux)
 
 lemma bin_to_bl_minus1_aux:
-  "bin_to_bl_aux n -1 bl = replicate n True @ bl"
+  "bin_to_bl_aux n (- 1) bl = replicate n True @ bl"
   by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)
 
-lemma bin_to_bl_minus1: "bin_to_bl n -1 = replicate n True"
+lemma bin_to_bl_minus1: "bin_to_bl n (- 1) = replicate n True"
   unfolding bin_to_bl_def by (simp add: bin_to_bl_minus1_aux)
 
 lemma bl_to_bin_rep_F: 
diff -r 24096e89c131 -r 6d46ad54a2ab src/HOL/Word/Examples/WordExamples.thy
--- a/src/HOL/Word/Examples/WordExamples.thy	Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Word/Examples/WordExamples.thy	Sun Sep 21 16:56:11 2014 +0200
@@ -33,13 +33,13 @@
   "27 + 11 = (6::5 word)"
   "7 * 3 = (21::'a::len word)"
   "11 - 27 = (-16::'a::len word)"
-  "- -11 = (11::'a::len word)"
+  "- (- 11) = (11::'a::len word)"
   "-40 + 1 = (-39::'a::len word)"
   by simp_all
 
 lemma "word_pred 2 = 1" by simp
 
-lemma "word_succ -3 = -2" by simp
+lemma "word_succ (- 3) = -2" by simp
   
 lemma "23 < (27::8 word)" by simp
 lemma "23 \<le> (27::8 word)" by simp
@@ -147,11 +147,11 @@
 lemma "word_rotr 2 0b0110 = (0b1001::4 word)" by simp
 lemma "word_rotl 1 0b1110 = (0b1101::4 word)" by simp
 lemma "word_roti 2 0b1110 = (0b1011::4 word)" by simp
-lemma "word_roti -2 0b0110 = (0b1001::4 word)" by simp
+lemma "word_roti (- 2) 0b0110 = (0b1001::4 word)" by simp
 lemma "word_rotr 2 0 = (0::4 word)" by simp
 lemma "word_rotr 2 1 = (0b0100::4 word)" apply simp? oops
 lemma "word_rotl 2 1 = (0b0100::4 word)" apply simp? oops
-lemma "word_roti -2 1 = (0b0100::4 word)" apply simp? oops
+lemma "word_roti (- 2) 1 = (0b0100::4 word)" apply simp? oops
 
 lemma "(x AND 0xff00) OR (x AND 0x00ff) = (x::16 word)"
 proof -
diff -r 24096e89c131 -r 6d46ad54a2ab src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Word/Word.thy	Sun Sep 21 16:56:11 2014 +0200
@@ -1275,7 +1275,7 @@
 lemma scast_0 [simp]: "scast 0 = 0"
   unfolding scast_def by simp
 
-lemma sint_n1 [simp] : "sint -1 = -1"
+lemma sint_n1 [simp] : "sint (- 1) = - 1"
   unfolding word_m1_wi word_sbin.eq_norm by simp
 
 lemma scast_n1 [simp]: "scast (- 1) = - 1"
@@ -1349,7 +1349,7 @@
 lemmas uint_div_alt = word_div_def [THEN trans [OF uint_cong int_word_uint]]
 lemmas uint_mod_alt = word_mod_def [THEN trans [OF uint_cong int_word_uint]]
 
-lemma word_pred_0_n1: "word_pred 0 = word_of_int -1"
+lemma word_pred_0_n1: "word_pred 0 = word_of_int (- 1)"
   unfolding word_pred_m1 by simp
 
 lemma succ_pred_no [simp]:
@@ -1360,7 +1360,7 @@
   unfolding word_succ_p1 word_pred_m1 by simp_all
 
 lemma word_sp_01 [simp] : 
-  "word_succ -1 = 0 & word_succ 0 = 1 & word_pred 0 = -1 & word_pred 1 = 0"
+  "word_succ (- 1) = 0 & word_succ 0 = 1 & word_pred 0 = - 1 & word_pred 1 = 0"
   unfolding word_succ_p1 word_pred_m1 by simp_all
 
 (* alternative approach to lifting arithmetic equalities *)
@@ -2803,7 +2803,7 @@
 lemma sshiftr1_0 [simp]: "sshiftr1 0 = 0"
   unfolding sshiftr1_def by simp
 
-lemma sshiftr1_n1 [simp] : "sshiftr1 -1 = -1"
+lemma sshiftr1_n1 [simp] : "sshiftr1 (- 1) = - 1"
   unfolding sshiftr1_def by simp
 
 lemma shiftl_0 [simp] : "(0::'a::len0 word) << n = 0"
@@ -3243,7 +3243,7 @@
 lemma mask_bl: "mask n = of_bl (replicate n True)"
   by (auto simp add : test_bit_of_bl word_size intro: word_eqI)
 
-lemma mask_bin: "mask n = word_of_int (bintrunc n -1)"
+lemma mask_bin: "mask n = word_of_int (bintrunc n (- 1))"
   by (auto simp add: nth_bintr word_size intro: word_eqI)
 
 lemma and_mask_bintr: "w AND mask n = word_of_int (bintrunc n (uint w))"
@@ -4729,7 +4729,7 @@
 done
 
 lemma word_rec_max: 
-  "\<forall>m\<ge>n. m \<noteq> -1 \<longrightarrow> f m = id \<Longrightarrow> word_rec z f -1 = word_rec z f n"
+  "\<forall>m\<ge>n. m \<noteq> - 1 \<longrightarrow> f m = id \<Longrightarrow> word_rec z f (- 1) = word_rec z f n"
 apply (subst word_rec_twice[where n="-1" and m="-1 - n"])
  apply simp
 apply simp
diff -r 24096e89c131 -r 6d46ad54a2ab src/HOL/ex/BinEx.thy
--- a/src/HOL/ex/BinEx.thy	Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/ex/BinEx.thy	Sun Sep 21 16:56:11 2014 +0200
@@ -98,7 +98,7 @@
 lemma "!!a::int. [| a+b <= i+j; a<=b; i<=j |] ==> a+a <= j+j"
 by arith
 
-lemma "!!a::int. [| a+b < i+j; a<b; i<j |] ==> a+a - - -1 < j+j - 3"
+lemma "!!a::int. [| a+b < i+j; a<b; i<j |] ==> a+a - - (- 1) < j+j - 3"
 by arith
 
 lemma "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k"
@@ -262,7 +262,7 @@
 lemma "2 ^ 10 = (1024::int)"
   by simp
 
-lemma "-3 ^ 7 = (-2187::int)"
+lemma "(- 3) ^ 7 = (-2187::int)"
   by simp
 
 lemma "13 ^ 7 = (62748517::int)"
@@ -271,7 +271,7 @@
 lemma "3 ^ 15 = (14348907::int)"
   by simp
 
-lemma "-5 ^ 11 = (-48828125::int)"
+lemma "(- 5) ^ 11 = (-48828125::int)"
   by simp
 
 
@@ -446,7 +446,7 @@
 lemma "2 ^ 15 = (32768::real)"
 by simp
 
-lemma "-3 ^ 7 = (-2187::real)"
+lemma "(- 3) ^ 7 = (-2187::real)"
 by simp
 
 lemma "13 ^ 7 = (62748517::real)"
@@ -455,7 +455,7 @@
 lemma "3 ^ 15 = (14348907::real)"
 by simp
 
-lemma "-5 ^ 11 = (-48828125::real)"
+lemma "(- 5) ^ 11 = (-48828125::real)"
 by simp
 
 
diff -r 24096e89c131 -r 6d46ad54a2ab src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Sun Sep 21 16:56:06 2014 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Sun Sep 21 16:56:11 2014 +0200
@@ -98,9 +98,8 @@
 val scan_tid = $$$ "'" @@@ scan_id;
 
 val scan_nat = Scan.many1 (Symbol.is_digit o Symbol_Pos.symbol);
+val scan_float = scan_nat @@@ $$$ "." @@@ scan_nat;
 val scan_int = $$$ "-" @@@ scan_nat || scan_nat;
-val scan_natdot = scan_nat @@@ $$$ "." @@@ scan_nat;
-val scan_float = $$$ "-" @@@ scan_natdot || scan_natdot;
 val scan_hex = $$$ "0" @@@ $$$ "x" @@@ Scan.many1 (Symbol.is_ascii_hex o Symbol_Pos.symbol);
 val scan_bin = $$$ "0" @@@ $$$ "b" @@@ Scan.many1 (fn (s, _) => s = "0" orelse s = "1");
 
@@ -264,15 +263,16 @@
       (if xids then $$$ "_" @@@ scan_id || scan_id else scan_id) ||
       $$$ "_" @@@ $$$ "_";
 
-    val scan_num = scan_hex || scan_bin || scan_int;
+    val scan_num_unsigned = scan_hex || scan_bin || scan_nat;
+    val scan_num_signed = scan_hex || scan_bin || scan_int;
 
     val scan_val =
       scan_tvar >> token TVarSy ||
       scan_var >> token VarSy ||
       scan_tid >> token TFreeSy ||
       scan_float >> token FloatSy ||
-      scan_num >> token NumSy ||
-      $$$ "#" @@@ scan_num >> token XNumSy ||
+      scan_num_unsigned >> token NumSy ||
+      $$$ "#" @@@ scan_num_signed >> token XNumSy ||
       scan_longid >> token LongIdentSy ||
       scan_xid >> token IdentSy;