# HG changeset patch
# User wenzelm
# Date 1376848759 -7200
# Node ID a1b3784f81294a284a78a7c0722b16feb44fe60e
# Parent  47c9aff07725b6efe5c55cbdd8cbeb6240c77059
more symbols;

diff -r 47c9aff07725 -r a1b3784f8129 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Sun Aug 18 19:59:19 2013 +0200
@@ -234,10 +234,10 @@
   assumes "sqrt x < b" and "0 < b" and "0 < x"
   shows "sqrt x < (b + x / b)/2"
 proof -
-  from assms have "0 < (b - sqrt x) ^ 2 " by simp
-  also have "\<dots> = b ^ 2 - 2 * b * sqrt x + (sqrt x) ^ 2" by algebra
-  also have "\<dots> = b ^ 2 - 2 * b * sqrt x + x" using assms by simp
-  finally have "0 < b ^ 2 - 2 * b * sqrt x + x" by assumption
+  from assms have "0 < (b - sqrt x)\<^sup>2 " by simp
+  also have "\<dots> = b\<^sup>2 - 2 * b * sqrt x + (sqrt x)\<^sup>2" by algebra
+  also have "\<dots> = b\<^sup>2 - 2 * b * sqrt x + x" using assms by simp
+  finally have "0 < b\<^sup>2 - 2 * b * sqrt x + x" .
   hence "0 < b / 2 - sqrt x + x / (2 * b)" using assms
     by (simp add: field_simps power2_eq_square)
   thus ?thesis by (simp add: field_simps)
diff -r 47c9aff07725 -r a1b3784f8129 src/HOL/Decision_Procs/Commutative_Ring.thy
--- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Sun Aug 18 19:59:19 2013 +0200
@@ -287,7 +287,7 @@
             by (simp only: numerals even_nat_div_two_times_two [OF `even w`])
           have "Ipol ls P * Ipol ls P = Ipol ls P ^ Suc (Suc 0)"
             by simp
-          then have "Ipol ls P * Ipol ls P = Ipol ls P ^ 2"
+          then have "Ipol ls P * Ipol ls P = (Ipol ls P)\<^sup>2"
             by (simp add: numerals)
           with Suc show ?thesis
             by (auto simp add: power_mult [symmetric, of _ 2 _] two_times mul_ci sqr_ci
diff -r 47c9aff07725 -r a1b3784f8129 src/HOL/Decision_Procs/ex/Approximation_Ex.thy
--- a/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Sun Aug 18 19:59:19 2013 +0200
@@ -72,7 +72,7 @@
   shows "g / v * tan (35 * d) \<in> { 3 * d .. 3.1 * d }"
   using assms by (approximation 20)
 
-lemma "x \<in> { 0 .. 1 :: real } \<longrightarrow> x ^ 2 \<le> x"
+lemma "x \<in> { 0 .. 1 :: real } \<longrightarrow> x\<^sup>2 \<le> x"
   by (approximation 30 splitting: x=1 taylor: x = 3)
 
 value [approximate] "10"
diff -r 47c9aff07725 -r a1b3784f8129 src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy	Sun Aug 18 19:59:19 2013 +0200
@@ -1173,22 +1173,22 @@
 lemma fps_inverse_deriv:
   fixes a:: "('a :: field) fps"
   assumes a0: "a$0 \<noteq> 0"
-  shows "fps_deriv (inverse a) = - fps_deriv a * inverse a ^ 2"
+  shows "fps_deriv (inverse a) = - fps_deriv a * (inverse a)\<^sup>2"
 proof-
   from inverse_mult_eq_1[OF a0]
   have "fps_deriv (inverse a * a) = 0" by simp
   hence "inverse a * fps_deriv a + fps_deriv (inverse a) * a = 0" by simp
   hence "inverse a * (inverse a * fps_deriv a + fps_deriv (inverse a) * a) = 0"  by simp
   with inverse_mult_eq_1[OF a0]
-  have "inverse a ^ 2 * fps_deriv a + fps_deriv (inverse a) = 0"
+  have "(inverse a)\<^sup>2 * fps_deriv a + fps_deriv (inverse a) = 0"
     unfolding power2_eq_square
     apply (simp add: field_simps)
     apply (simp add: mult_assoc[symmetric])
     done
-  then have "inverse a ^ 2 * fps_deriv a + fps_deriv (inverse a) - fps_deriv a * inverse a ^ 2 =
-      0 - fps_deriv a * inverse a ^ 2"
+  then have "(inverse a)\<^sup>2 * fps_deriv a + fps_deriv (inverse a) - fps_deriv a * (inverse a)\<^sup>2 =
+      0 - fps_deriv a * (inverse a)\<^sup>2"
     by simp
-  then show "fps_deriv (inverse a) = - fps_deriv a * inverse a ^ 2"
+  then show "fps_deriv (inverse a) = - fps_deriv a * (inverse a)\<^sup>2"
     by (simp add: field_simps)
 qed
 
@@ -1223,7 +1223,7 @@
 lemma fps_inverse_deriv':
   fixes a:: "('a :: field) fps"
   assumes a0: "a$0 \<noteq> 0"
-  shows "fps_deriv (inverse a) = - fps_deriv a / a ^ 2"
+  shows "fps_deriv (inverse a) = - fps_deriv a / a\<^sup>2"
   using fps_inverse_deriv[OF a0]
   unfolding power2_eq_square fps_divide_def fps_inverse_mult
   by simp
@@ -1236,7 +1236,7 @@
 lemma fps_divide_deriv:
   fixes a:: "('a :: field) fps"
   assumes a0: "b$0 \<noteq> 0"
-  shows "fps_deriv (a / b) = (fps_deriv a * b - a * fps_deriv b) / b ^ 2"
+  shows "fps_deriv (a / b) = (fps_deriv a * b - a * fps_deriv b) / b\<^sup>2"
   using fps_inverse_deriv[OF a0]
   by (simp add: fps_divide_def field_simps
     power2_eq_square fps_inverse_mult inverse_mult_eq_1'[OF a0])
@@ -3210,7 +3210,7 @@
   apply (simp only: binomial_gbinomial[symmetric] of_nat_mult[symmetric] of_nat_setsum[symmetric] of_nat_add[symmetric])
   by simp
 
-lemma binomial_Vandermonde_same: "setsum (\<lambda>k. (n choose k)^2) {0..n} = (2*n) choose n"
+lemma binomial_Vandermonde_same: "setsum (\<lambda>k. (n choose k)\<^sup>2) {0..n} = (2*n) choose n"
   using binomial_Vandermonde[of n n n,symmetric]
   unfolding mult_2 apply (simp add: power2_eq_square)
   apply (rule setsum_cong2)
@@ -3425,8 +3425,8 @@
 qed
 
 lemma fps_sin_cos_sum_of_squares:
-  "fps_cos c ^ 2 + fps_sin c ^ 2 = 1" (is "?lhs = 1")
-proof-
+  "(fps_cos c)\<^sup>2 + (fps_sin c)\<^sup>2 = 1" (is "?lhs = 1")
+proof -
   have "fps_deriv ?lhs = 0"
     apply (simp add:  fps_deriv_power fps_sin_deriv fps_cos_deriv)
     apply (simp add: field_simps fps_const_neg[symmetric] del: fps_const_neg)
@@ -3546,7 +3546,7 @@
 
 definition "fps_tan c = fps_sin c / fps_cos c"
 
-lemma fps_tan_deriv: "fps_deriv(fps_tan c) = fps_const c/ (fps_cos c ^ 2)"
+lemma fps_tan_deriv: "fps_deriv (fps_tan c) = fps_const c / (fps_cos c)\<^sup>2"
 proof -
   have th0: "fps_cos c $ 0 \<noteq> 0" by (simp add: fps_cos_def)
   show ?thesis
diff -r 47c9aff07725 -r a1b3784f8129 src/HOL/Library/Fundamental_Theorem_Algebra.thy
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sun Aug 18 19:59:19 2013 +0200
@@ -14,7 +14,7 @@
            else Complex (sqrt((cmod z + Re z) /2))
                         ((Im z / abs(Im z)) * sqrt((cmod z - Re z) /2)))"
 
-lemma csqrt[algebra]: "csqrt z ^ 2 = z"
+lemma csqrt[algebra]: "(csqrt z)\<^sup>2 = z"
 proof-
   obtain x y where xy: "z = Complex x y" by (cases z)
   {assume y0: "y = 0"
@@ -34,13 +34,15 @@
       hence "cmod ?z - x \<ge> 0" "cmod ?z + x \<ge> 0" by arith+
       hence "(sqrt (x * x + y * y) + x) / 2 \<ge> 0" "(sqrt (x * x + y * y) - x) / 2 \<ge> 0" by (simp_all add: power2_eq_square) }
     note th = this
-    have sq4: "\<And>x::real. x^2 / 4 = (x / 2) ^ 2"
+    have sq4: "\<And>x::real. x\<^sup>2 / 4 = (x / 2)\<^sup>2"
       by (simp add: power2_eq_square)
     from th[of x y]
-    have sq4': "sqrt (((sqrt (x * x + y * y) + x)^2 / 4)) = (sqrt (x * x + y * y) + x) / 2" "sqrt (((sqrt (x * x + y * y) - x)^2 / 4)) = (sqrt (x * x + y * y) - x) / 2" unfolding sq4 by simp_all
+    have sq4': "sqrt (((sqrt (x * x + y * y) + x)\<^sup>2 / 4)) = (sqrt (x * x + y * y) + x) / 2"
+      "sqrt (((sqrt (x * x + y * y) - x)\<^sup>2 / 4)) = (sqrt (x * x + y * y) - x) / 2"
+      unfolding sq4 by simp_all
     then have th1: "sqrt ((sqrt (x * x + y * y) + x) * (sqrt (x * x + y * y) + x) / 4) - sqrt ((sqrt (x * x + y * y) - x) * (sqrt (x * x + y * y) - x) / 4) = x"
       unfolding power2_eq_square by simp
-    have "sqrt 4 = sqrt (2^2)" by simp
+    have "sqrt 4 = sqrt (2\<^sup>2)" by simp
     hence sqrt4: "sqrt 4 = 2" by (simp only: real_sqrt_abs)
     have th2: "2 *(y * sqrt ((sqrt (x * x + y * y) - x) * (sqrt (x * x + y * y) + x) / 4)) / \<bar>y\<bar> = y"
       using iffD2[OF real_sqrt_pow2_iff sum_power2_ge_zero[of x y]] y0
@@ -184,14 +186,14 @@
   shows "cmod (z + 1) < 1 \<or> cmod (z - 1) < 1 \<or> cmod (z + ii) < 1 \<or> cmod (z - ii) < 1"
 proof-
   obtain x y where z: "z = Complex x y " by (cases z, auto)
-  from md z have xy: "x^2 + y^2 = 1" by (simp add: cmod_def)
+  from md z have xy: "x\<^sup>2 + y\<^sup>2 = 1" by (simp add: cmod_def)
   {assume C: "cmod (z + 1) \<ge> 1" "cmod (z - 1) \<ge> 1" "cmod (z + ii) \<ge> 1" "cmod (z - ii) \<ge> 1"
     from C z xy have "2*x \<le> 1" "2*x \<ge> -1" "2*y \<le> 1" "2*y \<ge> -1"
       by (simp_all add: cmod_def power2_eq_square algebra_simps)
     hence "abs (2*x) \<le> 1" "abs (2*y) \<le> 1" by simp_all
-    hence "(abs (2 * x))^2 <= 1^2" "(abs (2 * y)) ^2 <= 1^2"
+    hence "(abs (2 * x))\<^sup>2 <= 1\<^sup>2" "(abs (2 * y))\<^sup>2 <= 1\<^sup>2"
       by - (rule power_mono, simp, simp)+
-    hence th0: "4*x^2 \<le> 1" "4*y^2 \<le> 1"
+    hence th0: "4*x\<^sup>2 \<le> 1" "4*y\<^sup>2 \<le> 1"
       by (simp_all add: power_mult_distrib)
     from add_mono[OF th0] xy have False by simp }
   thus ?thesis unfolding linorder_not_le[symmetric] by blast
@@ -454,7 +456,7 @@
   ultimately show ?thesis by blast
 qed
 
-lemma "(rcis (sqrt (abs r)) (a/2)) ^ 2 = rcis (abs r) a"
+lemma "(rcis (sqrt (abs r)) (a/2))\<^sup>2 = rcis (abs r) a"
   unfolding power2_eq_square
   apply (simp add: rcis_mult)
   apply (simp add: power2_eq_square[symmetric])
@@ -464,7 +466,7 @@
   unfolding cis_def
   by simp
 
-lemma "(rcis (sqrt (abs r)) ((pi + a)/2)) ^ 2 = rcis (- abs r) a"
+lemma "(rcis (sqrt (abs r)) ((pi + a)/2))\<^sup>2 = rcis (- abs r) a"
   unfolding power2_eq_square
   apply (simp add: rcis_mult add_divide_distrib)
   apply (simp add: power2_eq_square[symmetric] rcis_def cispi cis_mult[symmetric])
diff -r 47c9aff07725 -r a1b3784f8129 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sun Aug 18 19:59:19 2013 +0200
@@ -3361,7 +3361,7 @@
       thus False using y[THEN bspec[where x="y + u *\<^sub>R (x - y)"]]
         using assms(1)[unfolded convex_alt, THEN bspec[where x=y]]
         using `x\<in>s` `y\<in>s` by (auto simp add: dist_commute algebra_simps) qed
-    moreover have "0 < norm (y - z) ^ 2" using `y\<in>s` `z\<notin>s` by auto
+    moreover have "0 < (norm (y - z))\<^sup>2" using `y\<in>s` `z\<notin>s` by auto
     hence "0 < inner (y - z) (y - z)" unfolding power2_norm_eq_inner by simp
     ultimately show "inner (y - z) z + (norm (y - z))\<^sup>2 / 2 < inner (y - z) x"
       unfolding power2_norm_eq_inner and not_less by (auto simp add: field_simps inner_commute inner_diff)
diff -r 47c9aff07725 -r a1b3784f8129 src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Sun Aug 18 19:59:19 2013 +0200
@@ -629,7 +629,7 @@
   then guess x .. note x=this
   show ?thesis proof(cases "f a = f b")
     case False
-    have "norm (f b - f a) * norm (f b - f a) = norm (f b - f a)^2"
+    have "norm (f b - f a) * norm (f b - f a) = (norm (f b - f a))\<^sup>2"
       by (simp add: power2_eq_square)
     also have "\<dots> = (f b - f a) \<bullet> (f b - f a)" unfolding power2_norm_eq_inner ..
     also have "\<dots> = (f b - f a) \<bullet> f' x (b - a)"
diff -r 47c9aff07725 -r a1b3784f8129 src/HOL/Multivariate_Analysis/Determinants.thy
--- a/src/HOL/Multivariate_Analysis/Determinants.thy	Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy	Sun Aug 18 19:59:19 2013 +0200
@@ -917,7 +917,7 @@
   {fix v w
     {fix x note fd[rule_format, of x 0, unfolded dist_norm f0 diff_0_right] }
     note th0 = this
-    have "f v \<bullet> f w = c^2 * (v \<bullet> w)"
+    have "f v \<bullet> f w = c\<^sup>2 * (v \<bullet> w)"
       unfolding dot_norm_neg dist_norm[symmetric]
       unfolding th0 fd[rule_format] by (simp add: power2_eq_square field_simps)}
   note fc = this
diff -r 47c9aff07725 -r a1b3784f8129 src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Sun Aug 18 19:59:19 2013 +0200
@@ -17,7 +17,7 @@
 
 lemma square_bound_lemma: "(x::real) < (1 + x) * (1 + x)"
 proof -
-  have "(x + 1/2)^2 + 3/4 > 0" using zero_le_power2[of "x+1/2"] by arith
+  have "(x + 1/2)\<^sup>2 + 3/4 > 0" using zero_le_power2[of "x+1/2"] by arith
   then show ?thesis by (simp add: field_simps power2_eq_square)
 qed
 
@@ -30,21 +30,21 @@
   apply auto
   done
 
-lemma real_le_lsqrt: "0 <= x \<Longrightarrow> 0 <= y \<Longrightarrow> x <= y^2 ==> sqrt x <= y"
-  using real_sqrt_le_iff[of x "y^2"] by simp
-
-lemma real_le_rsqrt: "x^2 \<le> y \<Longrightarrow> x \<le> sqrt y"
-  using real_sqrt_le_mono[of "x^2" y] by simp
-
-lemma real_less_rsqrt: "x^2 < y \<Longrightarrow> x < sqrt y"
-  using real_sqrt_less_mono[of "x^2" y] by simp
+lemma real_le_lsqrt: "0 <= x \<Longrightarrow> 0 <= y \<Longrightarrow> x <= y\<^sup>2 ==> sqrt x <= y"
+  using real_sqrt_le_iff[of x "y\<^sup>2"] by simp
+
+lemma real_le_rsqrt: "x\<^sup>2 \<le> y \<Longrightarrow> x \<le> sqrt y"
+  using real_sqrt_le_mono[of "x\<^sup>2" y] by simp
+
+lemma real_less_rsqrt: "x\<^sup>2 < y \<Longrightarrow> x < sqrt y"
+  using real_sqrt_less_mono[of "x\<^sup>2" y] by simp
 
 lemma sqrt_even_pow2:
   assumes n: "even n"
   shows "sqrt(2 ^ n) = 2 ^ (n div 2)"
 proof -
   from n obtain m where m: "n = 2*m" unfolding even_mult_two_ex ..
-  from m  have "sqrt(2 ^ n) = sqrt ((2 ^ m) ^ 2)"
+  from m  have "sqrt(2 ^ n) = sqrt ((2 ^ m)\<^sup>2)"
     by (simp only: power_mult[symmetric] mult_commute)
   then show ?thesis  using m by simp
 qed
@@ -85,13 +85,13 @@
 
 text{* Squaring equations and inequalities involving norms.  *}
 
-lemma dot_square_norm: "x \<bullet> x = norm(x)^2"
+lemma dot_square_norm: "x \<bullet> x = (norm x)\<^sup>2"
   by (simp only: power2_norm_eq_inner) (* TODO: move? *)
 
-lemma norm_eq_square: "norm(x) = a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x = a^2"
+lemma norm_eq_square: "norm(x) = a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x = a\<^sup>2"
   by (auto simp add: norm_eq_sqrt_inner)
 
-lemma real_abs_le_square_iff: "\<bar>x\<bar> \<le> \<bar>y\<bar> \<longleftrightarrow> (x::real)^2 \<le> y^2"
+lemma real_abs_le_square_iff: "\<bar>x\<bar> \<le> \<bar>y\<bar> \<longleftrightarrow> (x::real)\<^sup>2 \<le> y\<^sup>2"
 proof
   assume "\<bar>x\<bar> \<le> \<bar>y\<bar>"
   then have "\<bar>x\<bar>\<^sup>2 \<le> \<bar>y\<bar>\<^sup>2" by (rule power_mono, simp)
@@ -102,21 +102,21 @@
   then show "\<bar>x\<bar> \<le> \<bar>y\<bar>" by simp
 qed
 
-lemma norm_le_square: "norm(x) <= a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x <= a^2"
+lemma norm_le_square: "norm(x) <= a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x <= a\<^sup>2"
   apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric])
   using norm_ge_zero[of x]
   apply arith
   done
 
-lemma norm_ge_square: "norm(x) >= a \<longleftrightarrow> a <= 0 \<or> x \<bullet> x >= a ^ 2"
+lemma norm_ge_square: "norm(x) >= a \<longleftrightarrow> a <= 0 \<or> x \<bullet> x >= a\<^sup>2"
   apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric])
   using norm_ge_zero[of x]
   apply arith
   done
 
-lemma norm_lt_square: "norm(x) < a \<longleftrightarrow> 0 < a \<and> x \<bullet> x < a^2"
+lemma norm_lt_square: "norm(x) < a \<longleftrightarrow> 0 < a \<and> x \<bullet> x < a\<^sup>2"
   by (metis not_le norm_ge_square)
-lemma norm_gt_square: "norm(x) > a \<longleftrightarrow> a < 0 \<or> x \<bullet> x > a^2"
+lemma norm_gt_square: "norm(x) > a \<longleftrightarrow> a < 0 \<or> x \<bullet> x > a\<^sup>2"
   by (metis norm_le_square not_less)
 
 text{* Dot product in terms of the norm rather than conversely. *}
@@ -124,10 +124,10 @@
 lemmas inner_simps = inner_add_left inner_add_right inner_diff_right inner_diff_left 
   inner_scaleR_left inner_scaleR_right
 
-lemma dot_norm: "x \<bullet> y = (norm(x + y) ^2 - norm x ^ 2 - norm y ^ 2) / 2"
+lemma dot_norm: "x \<bullet> y = ((norm (x + y))\<^sup>2 - (norm x)\<^sup>2 - (norm y)\<^sup>2) / 2"
   unfolding power2_norm_eq_inner inner_simps inner_commute by auto 
 
-lemma dot_norm_neg: "x \<bullet> y = ((norm x ^ 2 + norm y ^ 2) - norm(x - y) ^ 2) / 2"
+lemma dot_norm_neg: "x \<bullet> y = (((norm x)\<^sup>2 + (norm y)\<^sup>2) - (norm (x - y))\<^sup>2) / 2"
   unfolding power2_norm_eq_inner inner_simps inner_commute
   by (auto simp add: algebra_simps)
 
@@ -469,11 +469,11 @@
 
 
 lemma triangle_lemma:
-  assumes x: "0 <= (x::real)" and y:"0 <= y" and z: "0 <= z" and xy: "x^2 <= y^2 + z^2"
+  assumes x: "0 <= (x::real)" and y:"0 <= y" and z: "0 <= z" and xy: "x\<^sup>2 <= y\<^sup>2 + z\<^sup>2"
   shows "x <= y + z"
 proof -
-  have "y^2 + z^2 \<le> y^2 + 2*y*z + z^2" using z y by (simp add: mult_nonneg_nonneg)
-  with xy have th: "x ^2 \<le> (y+z)^2" by (simp add: power2_eq_square field_simps)
+  have "y\<^sup>2 + z\<^sup>2 \<le> y\<^sup>2 + 2*y*z + z\<^sup>2" using z y by (simp add: mult_nonneg_nonneg)
+  with xy have th: "x\<^sup>2 \<le> (y+z)\<^sup>2" by (simp add: power2_eq_square field_simps)
   from y z have yz: "y + z \<ge> 0" by arith
   from power2_le_imp_le[OF th yz] show ?thesis .
 qed
@@ -2592,11 +2592,11 @@
 proof -
   let ?d = "DIM('a)"
   have "real ?d \<ge> 0" by simp
-  then have d2: "(sqrt (real ?d))^2 = real ?d"
+  then have d2: "(sqrt (real ?d))\<^sup>2 = real ?d"
     by (auto intro: real_sqrt_pow2)
   have th: "sqrt (real ?d) * infnorm x \<ge> 0"
     by (simp add: zero_le_mult_iff infnorm_pos_le)
-  have th1: "x \<bullet> x \<le> (sqrt (real ?d) * infnorm x)^2"
+  have th1: "x \<bullet> x \<le> (sqrt (real ?d) * infnorm x)\<^sup>2"
     unfolding power_mult_distrib d2
     unfolding real_of_nat_def
     apply(subst euclidean_inner)
@@ -2680,9 +2680,9 @@
       by simp_all
     then have n: "norm x > 0" "norm y > 0"
       using norm_ge_zero[of x] norm_ge_zero[of y] by arith+
-    have th: "\<And>(a::real) b c. a + b + c \<noteq> 0 ==> (a = b + c \<longleftrightarrow> a^2 = (b + c)^2)"
+    have th: "\<And>(a::real) b c. a + b + c \<noteq> 0 ==> (a = b + c \<longleftrightarrow> a\<^sup>2 = (b + c)\<^sup>2)"
       by algebra
-    have "norm(x + y) = norm x + norm y \<longleftrightarrow> norm(x + y)^ 2 = (norm x + norm y) ^2"
+    have "norm (x + y) = norm x + norm y \<longleftrightarrow> (norm (x + y))\<^sup>2 = (norm x + norm y)\<^sup>2"
       apply (rule th) using n norm_ge_zero[of "x + y"]
       apply arith
       done
diff -r 47c9aff07725 -r a1b3784f8129 src/HOL/NSA/CLim.thy
--- a/src/HOL/NSA/CLim.thy	Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/NSA/CLim.thy	Sun Aug 18 19:59:19 2013 +0200
@@ -15,7 +15,7 @@
 
 (*??generalize*)
 lemma lemma_complex_mult_inverse_squared [simp]:
-     "x \<noteq> (0::complex) \<Longrightarrow> (x * inverse(x) ^ 2) = inverse x"
+     "x \<noteq> (0::complex) \<Longrightarrow> x * (inverse x)\<^sup>2 = inverse x"
 by (simp add: numeral_2_eq_2)
 
 text{*Changing the quantified variable. Install earlier?*}
@@ -152,12 +152,12 @@
 
 text{*Can't relax the premise @{term "x \<noteq> 0"}: it isn't continuous at zero*}
 lemma NSCDERIV_inverse:
-     "(x::complex) \<noteq> 0 ==> NSDERIV (%x. inverse(x)) x :> (- (inverse x ^ 2))"
+     "(x::complex) \<noteq> 0 ==> NSDERIV (%x. inverse(x)) x :> (- ((inverse x)\<^sup>2))"
 unfolding numeral_2_eq_2
 by (rule NSDERIV_inverse)
 
 lemma CDERIV_inverse:
-     "(x::complex) \<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ 2))"
+     "(x::complex) \<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (- ((inverse x)\<^sup>2))"
 unfolding numeral_2_eq_2
 by (rule DERIV_inverse)
 
@@ -166,13 +166,13 @@
 
 lemma CDERIV_inverse_fun:
      "[| DERIV f x :> d; f(x) \<noteq> (0::complex) |]
-      ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))"
+      ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse ((f x)\<^sup>2)))"
 unfolding numeral_2_eq_2
 by (rule DERIV_inverse_fun)
 
 lemma NSCDERIV_inverse_fun:
      "[| NSDERIV f x :> d; f(x) \<noteq> (0::complex) |]
-      ==> NSDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))"
+      ==> NSDERIV (%x. inverse(f x)) x :> (- (d * inverse ((f x)\<^sup>2)))"
 unfolding numeral_2_eq_2
 by (rule NSDERIV_inverse_fun)
 
@@ -181,13 +181,13 @@
 
 lemma CDERIV_quotient:
      "[| DERIV f x :> d; DERIV g x :> e; g(x) \<noteq> (0::complex) |]
-       ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ 2)"
+       ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / ((g x)\<^sup>2)"
 unfolding numeral_2_eq_2
 by (rule DERIV_quotient)
 
 lemma NSCDERIV_quotient:
      "[| NSDERIV f x :> d; NSDERIV g x :> e; g(x) \<noteq> (0::complex) |]
-       ==> NSDERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ 2)"
+       ==> NSDERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / ((g x)\<^sup>2)"
 unfolding numeral_2_eq_2
 by (rule NSDERIV_quotient)
 
diff -r 47c9aff07725 -r a1b3784f8129 src/HOL/NSA/HTranscendental.thy
--- a/src/HOL/NSA/HTranscendental.thy	Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/NSA/HTranscendental.thy	Sun Aug 18 19:59:19 2013 +0200
@@ -103,7 +103,7 @@
 lemma hypreal_sqrt_ge_zero: "0 \<le> x ==> 0 \<le> ( *f* sqrt)(x)"
 by (auto intro: hypreal_sqrt_gt_zero simp add: order_le_less)
 
-lemma hypreal_sqrt_hrabs [simp]: "!!x. ( *f* sqrt)(x ^ 2) = abs(x)"
+lemma hypreal_sqrt_hrabs [simp]: "!!x. ( *f* sqrt)(x\<^sup>2) = abs(x)"
 by (transfer, simp)
 
 lemma hypreal_sqrt_hrabs2 [simp]: "!!x. ( *f* sqrt)(x*x) = abs(x)"
@@ -128,7 +128,7 @@
 apply (auto simp add: st_hrabs st_zero_le star_sqrt_HFinite)
 done
 
-lemma hypreal_sqrt_sum_squares_ge1 [simp]: "!!x y. x \<le> ( *f* sqrt)(x ^ 2 + y ^ 2)"
+lemma hypreal_sqrt_sum_squares_ge1 [simp]: "!!x y. x \<le> ( *f* sqrt)(x\<^sup>2 + y\<^sup>2)"
 by transfer (rule real_sqrt_sum_squares_ge1)
 
 lemma HFinite_hypreal_sqrt:
@@ -584,14 +584,14 @@
 text{*A familiar approximation to @{term "cos x"} when @{term x} is small*}
 
 lemma STAR_cos_Infinitesimal_approx:
-     "x \<in> Infinitesimal ==> ( *f* cos) x @= 1 - x ^ 2"
+     "x \<in> Infinitesimal ==> ( *f* cos) x @= 1 - x\<^sup>2"
 apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
 apply (auto simp add: Infinitesimal_approx_minus [symmetric] 
             diff_minus add_assoc [symmetric] numeral_2_eq_2)
 done
 
 lemma STAR_cos_Infinitesimal_approx2:
-     "x \<in> Infinitesimal ==> ( *f* cos) x @= 1 - (x ^ 2)/2"
+     "x \<in> Infinitesimal ==> ( *f* cos) x @= 1 - (x\<^sup>2)/2"
 apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
 apply (auto intro: Infinitesimal_SReal_divide 
             simp add: Infinitesimal_approx_minus [symmetric] numeral_2_eq_2)
diff -r 47c9aff07725 -r a1b3784f8129 src/HOL/NSA/NSComplex.thy
--- a/src/HOL/NSA/NSComplex.thy	Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/NSA/NSComplex.thy	Sun Aug 18 19:59:19 2013 +0200
@@ -325,7 +325,7 @@
 by transfer (rule complex_cnj_zero_iff)
 
 lemma hcomplex_mult_hcnj:
-     "!!z. z * hcnj z = hcomplex_of_hypreal (hRe(z) ^ 2 + hIm(z) ^ 2)"
+     "!!z. z * hcnj z = hcomplex_of_hypreal ((hRe z)\<^sup>2 + (hIm z)\<^sup>2)"
 by transfer (rule complex_mult_cnj)
 
 
@@ -339,7 +339,7 @@
      "hcmod (hcomplex_of_hypreal(hypreal_of_hypnat n)) = hypreal_of_hypnat n"
 by simp
 
-lemma hcmod_mult_hcnj: "!!z. hcmod(z * hcnj(z)) = hcmod(z) ^ 2"
+lemma hcmod_mult_hcnj: "!!z. hcmod(z * hcnj(z)) = (hcmod z)\<^sup>2"
 by transfer (rule complex_mod_mult_cnj)
 
 lemma hcmod_triangle_ineq2 [simp]:
@@ -358,7 +358,7 @@
 lemma hcomplexpow_Suc [simp]: "z ^ (Suc n) = (z::hcomplex) * (z ^ n)"
 by (rule power_Suc)
 
-lemma hcomplexpow_i_squared [simp]: "iii ^ 2 = -1"
+lemma hcomplexpow_i_squared [simp]: "iii\<^sup>2 = -1"
 by transfer (rule power2_i)
 
 lemma hcomplex_of_hypreal_pow:
@@ -405,7 +405,7 @@
 lemma hsgn_eq: "!!z. hsgn z = z / hcomplex_of_hypreal (hcmod z)"
 by transfer (rule sgn_eq)
 
-lemma hcmod_i: "!!x y. hcmod (HComplex x y) = ( *f* sqrt) (x ^ 2 + y ^ 2)"
+lemma hcmod_i: "!!x y. hcmod (HComplex x y) = ( *f* sqrt) (x\<^sup>2 + y\<^sup>2)"
 by transfer (rule complex_norm)
 
 lemma hcomplex_eq_cancel_iff1 [simp]:
@@ -435,8 +435,7 @@
 by transfer (rule Im_sgn)
 
 lemma HComplex_inverse:
-     "!!x y. inverse (HComplex x y) =
-      HComplex (x/(x ^ 2 + y ^ 2)) (-y/(x ^ 2 + y ^ 2))"
+     "!!x y. inverse (HComplex x y) = HComplex (x/(x\<^sup>2 + y\<^sup>2)) (-y/(x\<^sup>2 + y\<^sup>2))"
 by transfer (rule complex_inverse)
 
 lemma hRe_mult_i_eq[simp]:
diff -r 47c9aff07725 -r a1b3784f8129 src/HOL/Number_Theory/Fib.thy
--- a/src/HOL/Number_Theory/Fib.thy	Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/Number_Theory/Fib.thy	Sun Aug 18 19:59:19 2013 +0200
@@ -169,24 +169,24 @@
 *}
 
 lemma fib_Cassini_aux_int: "fib (int n + 2) * fib (int n) -
-    (fib (int n + 1))^2 = (-1)^(n + 1)"
+    (fib (int n + 1))\<^sup>2 = (-1)^(n + 1)"
   apply (induct n)
   apply (auto simp add: field_simps power2_eq_square fib_reduce_int power_add)
   done
 
 lemma fib_Cassini_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n -
-    (fib (n + 1))^2 = (-1)^(nat n + 1)"
+    (fib (n + 1))\<^sup>2 = (-1)^(nat n + 1)"
   by (insert fib_Cassini_aux_int [of "nat n"], auto)
 
 (*
 lemma fib_Cassini'_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n =
-    (fib (n + 1))^2 + (-1)^(nat n + 1)"
+    (fib (n + 1))\<^sup>2 + (-1)^(nat n + 1)"
   by (frule fib_Cassini_int, simp)
 *)
 
 lemma fib_Cassini'_int: "n >= 0 \<Longrightarrow> fib ((n::int) + 2) * fib n =
-  (if even n then tsub ((fib (n + 1))^2) 1
-   else (fib (n + 1))^2 + 1)"
+  (if even n then tsub ((fib (n + 1))\<^sup>2) 1
+   else (fib (n + 1))\<^sup>2 + 1)"
   apply (frule fib_Cassini_int, auto simp add: pos_int_even_equiv_nat_even)
   apply (subst tsub_eq)
   apply (insert fib_gr_0_int [of "n + 1"], force)
@@ -194,8 +194,8 @@
   done
 
 lemma fib_Cassini_nat: "fib ((n::nat) + 2) * fib n =
-    (if even n then (fib (n + 1))^2 - 1
-     else (fib (n + 1))^2 + 1)"
+    (if even n then (fib (n + 1))\<^sup>2 - 1
+     else (fib (n + 1))\<^sup>2 + 1)"
   by (rule fib_Cassini'_int [transferred, of n], auto)
 
 
diff -r 47c9aff07725 -r a1b3784f8129 src/HOL/Old_Number_Theory/Euler.thy
--- a/src/HOL/Old_Number_Theory/Euler.thy	Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/Old_Number_Theory/Euler.thy	Sun Aug 18 19:59:19 2013 +0200
@@ -75,7 +75,7 @@
     from this and a show ?thesis
       by (auto simp add: zcong_zmult_prop2)
   qed
-  then have "[j^2 = a] (mod p)" by (simp add: power2_eq_square)
+  then have "[j\<^sup>2 = a] (mod p)" by (simp add: power2_eq_square)
   with assms show False by (simp add: QuadRes_def)
 qed
 
@@ -269,7 +269,7 @@
 
 text {* \medskip Prove the final part of Euler's Criterion: *}
 
-lemma aux__1: "[| ~([x = 0] (mod p)); [y ^ 2 = x] (mod p)|] ==> ~(p dvd y)"
+lemma aux__1: "[| ~([x = 0] (mod p)); [y\<^sup>2 = x] (mod p)|] ==> ~(p dvd y)"
   by (metis dvdI power2_eq_square zcong_sym zcong_trans zcong_zero_equiv_div dvd_trans)
 
 lemma aux__2: "2 * nat((p - 1) div 2) =  nat (2 * ((p - 1) div 2))"
diff -r 47c9aff07725 -r a1b3784f8129 src/HOL/Old_Number_Theory/EvenOdd.thy
--- a/src/HOL/Old_Number_Theory/EvenOdd.thy	Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/Old_Number_Theory/EvenOdd.thy	Sun Aug 18 19:59:19 2013 +0200
@@ -175,9 +175,9 @@
     by (simp add: nat_mult_distrib)
   finally have "(-1::int)^nat x = (-1)^(2 * nat a)"
     by simp
-  also have "... = ((-1::int)^2)^ (nat a)"
+  also have "... = (-1::int)\<^sup>2 ^ nat a"
     by (simp add: zpower_zpower [symmetric])
-  also have "(-1::int)^2 = 1"
+  also have "(-1::int)\<^sup>2 = 1"
     by simp
   finally show ?thesis
     by simp
@@ -192,11 +192,11 @@
     by simp
   also from a have "nat (2 * a + 1) = 2 * nat a + 1"
     by (auto simp add: nat_mult_distrib nat_add_distrib)
-  finally have "(-1::int)^nat x = (-1)^(2 * nat a + 1)"
+  finally have "(-1::int) ^ nat x = (-1)^(2 * nat a + 1)"
     by simp
-  also have "... = ((-1::int)^2)^ (nat a) * (-1)^1"
+  also have "... = ((-1::int)\<^sup>2) ^ nat a * (-1)^1"
     by (auto simp add: power_mult power_add)
-  also have "(-1::int)^2 = 1"
+  also have "(-1::int)\<^sup>2 = 1"
     by simp
   finally show ?thesis
     by simp
diff -r 47c9aff07725 -r a1b3784f8129 src/HOL/Old_Number_Theory/Pocklington.thy
--- a/src/HOL/Old_Number_Theory/Pocklington.thy	Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/Old_Number_Theory/Pocklington.thy	Sun Aug 18 19:59:19 2013 +0200
@@ -940,32 +940,32 @@
 qed
 
 lemma prime_divisor_sqrt:
-  "prime n \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>d. d dvd n \<and> d^2 \<le> n \<longrightarrow> d = 1)"
+  "prime n \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>d. d dvd n \<and> d\<^sup>2 \<le> n \<longrightarrow> d = 1)"
 proof-
   {assume "n=0 \<or> n=1" hence ?thesis using prime_0 prime_1
     by (auto simp add: nat_power_eq_0_iff)}
   moreover
   {assume n: "n\<noteq>0" "n\<noteq>1"
     hence np: "n > 1" by arith
-    {fix d assume d: "d dvd n" "d^2 \<le> n" and H: "\<forall>m. m dvd n \<longrightarrow> m=1 \<or> m=n"
+    {fix d assume d: "d dvd n" "d\<^sup>2 \<le> n" and H: "\<forall>m. m dvd n \<longrightarrow> m=1 \<or> m=n"
       from H d have d1n: "d = 1 \<or> d=n" by blast
       {assume dn: "d=n"
-        have "n^2 > n*1" using n by (simp add: power2_eq_square)
+        have "n\<^sup>2 > n*1" using n by (simp add: power2_eq_square)
         with dn d(2) have "d=1" by simp}
       with d1n have "d = 1" by blast  }
     moreover
-    {fix d assume d: "d dvd n" and H: "\<forall>d'. d' dvd n \<and> d'^2 \<le> n \<longrightarrow> d' = 1"
+    {fix d assume d: "d dvd n" and H: "\<forall>d'. d' dvd n \<and> d'\<^sup>2 \<le> n \<longrightarrow> d' = 1"
       from d n have "d \<noteq> 0" apply - apply (rule ccontr) by simp
       hence dp: "d > 0" by simp
       from d[unfolded dvd_def] obtain e where e: "n= d*e" by blast
       from n dp e have ep:"e > 0" by simp
-      have "d^2 \<le> n \<or> e^2 \<le> n" using dp ep
+      have "d\<^sup>2 \<le> n \<or> e\<^sup>2 \<le> n" using dp ep
         by (auto simp add: e power2_eq_square mult_le_cancel_left)
       moreover
-      {assume h: "d^2 \<le> n"
+      {assume h: "d\<^sup>2 \<le> n"
         from H[rule_format, of d] h d have "d = 1" by blast}
       moreover
-      {assume h: "e^2 \<le> n"
+      {assume h: "e\<^sup>2 \<le> n"
         from e have "e dvd n" unfolding dvd_def by (simp add: mult_commute)
         with H[rule_format, of e] h have "e=1" by simp
         with e have "d = n" by simp}
@@ -974,7 +974,7 @@
   ultimately show ?thesis by auto
 qed
 lemma prime_prime_factor_sqrt:
-  "prime n \<longleftrightarrow> n \<noteq> 0 \<and> n \<noteq> 1 \<and> \<not> (\<exists>p. prime p \<and> p dvd n \<and> p^2 \<le> n)"
+  "prime n \<longleftrightarrow> n \<noteq> 0 \<and> n \<noteq> 1 \<and> \<not> (\<exists>p. prime p \<and> p dvd n \<and> p\<^sup>2 \<le> n)"
   (is "?lhs \<longleftrightarrow>?rhs")
 proof-
   {assume "n=0 \<or> n=1" hence ?thesis using prime_0 prime_1 by auto}
@@ -990,14 +990,14 @@
     }
     moreover
     {assume H: ?rhs
-      {fix d assume d: "d dvd n" "d^2 \<le> n" "d\<noteq>1"
+      {fix d assume d: "d dvd n" "d\<^sup>2 \<le> n" "d\<noteq>1"
         from prime_factor[OF d(3)]
         obtain p where p: "prime p" "p dvd d" by blast
         from n have np: "n > 0" by arith
         from d(1) n have "d \<noteq> 0" by - (rule ccontr, auto)
         hence dp: "d > 0" by arith
         from mult_mono[OF dvd_imp_le[OF p(2) dp] dvd_imp_le[OF p(2) dp]] d(2)
-        have "p^2 \<le> n" unfolding power2_eq_square by arith
+        have "p\<^sup>2 \<le> n" unfolding power2_eq_square by arith
         with H n p(1) dvd_trans[OF p(2) d(1)] have False  by blast}
       with n prime_divisor_sqrt  have ?lhs by auto}
     ultimately have ?thesis by blast }
@@ -1073,7 +1073,7 @@
 qed
 
 lemma pocklington:
-  assumes n: "n \<ge> 2" and nqr: "n - 1 = q*r" and sqr: "n \<le> q^2"
+  assumes n: "n \<ge> 2" and nqr: "n - 1 = q*r" and sqr: "n \<le> q\<^sup>2"
   and an: "[a^ (n - 1) = 1] (mod n)"
   and aq:"\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a^ ((n - 1) div p) - 1) n"
   shows "prime n"
@@ -1081,7 +1081,7 @@
 proof-
   let ?ths = "n \<noteq> 0 \<and> n \<noteq> 1 \<and> \<not> (\<exists>p. prime p \<and> p dvd n \<and> p\<^sup>2 \<le> n)"
   from n have n01: "n\<noteq>0" "n\<noteq>1" by arith+
-  {fix p assume p: "prime p" "p dvd n" "p^2 \<le> n"
+  {fix p assume p: "prime p" "p dvd n" "p\<^sup>2 \<le> n"
     from p(3) sqr have "p^(Suc 1) \<le> q^(Suc 1)" by (simp add: power2_eq_square)
     hence pq: "p \<le> q" unfolding exp_mono_le .
     from pocklington_lemma[OF n nqr an aq p(1,2)]  cong_1_divides
@@ -1093,7 +1093,7 @@
 
 (* Variant for application, to separate the exponentiation.                  *)
 lemma pocklington_alt:
-  assumes n: "n \<ge> 2" and nqr: "n - 1 = q*r" and sqr: "n \<le> q^2"
+  assumes n: "n \<ge> 2" and nqr: "n - 1 = q*r" and sqr: "n \<le> q\<^sup>2"
   and an: "[a^ (n - 1) = 1] (mod n)"
   and aq:"\<forall>p. prime p \<and> p dvd q \<longrightarrow> (\<exists>b. [a^((n - 1) div p) = b] (mod n) \<and> coprime (b - 1) n)"
   shows "prime n"
@@ -1205,7 +1205,7 @@
 
 
 lemma pocklington_primefact:
-  assumes n: "n \<ge> 2" and qrn: "q*r = n - 1" and nq2: "n \<le> q^2"
+  assumes n: "n \<ge> 2" and qrn: "q*r = n - 1" and nq2: "n \<le> q\<^sup>2"
   and arnb: "(a^r) mod n = b" and psq: "foldr op * ps 1 = q"
   and bqn: "(b^q) mod n = 1"
   and psp: "list_all (\<lambda>p. prime p \<and> coprime ((b^(q div p)) mod n - 1) n) ps"
diff -r 47c9aff07725 -r a1b3784f8129 src/HOL/Old_Number_Theory/Primes.thy
--- a/src/HOL/Old_Number_Theory/Primes.thy	Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/Old_Number_Theory/Primes.thy	Sun Aug 18 19:59:19 2013 +0200
@@ -56,39 +56,39 @@
 using power_inject_base[of x n y] by auto
 
 
-lemma even_square: assumes e: "even (n::nat)" shows "\<exists>x. n ^ 2 = 4*x"
+lemma even_square: assumes e: "even (n::nat)" shows "\<exists>x. n\<^sup>2 = 4*x"
 proof-
   from e have "2 dvd n" by presburger
   then obtain k where k: "n = 2*k" using dvd_def by auto
-  hence "n^2 = 4* (k^2)" by (simp add: power2_eq_square)
+  hence "n\<^sup>2 = 4 * k\<^sup>2" by (simp add: power2_eq_square)
   thus ?thesis by blast
 qed
 
-lemma odd_square: assumes e: "odd (n::nat)" shows "\<exists>x. n ^ 2 = 4*x + 1"
+lemma odd_square: assumes e: "odd (n::nat)" shows "\<exists>x. n\<^sup>2 = 4*x + 1"
 proof-
   from e have np: "n > 0" by presburger
   from e have "2 dvd (n - 1)" by presburger
   then obtain k where "n - 1 = 2*k" using dvd_def by auto
   hence k: "n = 2*k + 1"  using e by presburger 
-  hence "n^2 = 4* (k^2 + k) + 1" by algebra   
+  hence "n\<^sup>2 = 4* (k\<^sup>2 + k) + 1" by algebra   
   thus ?thesis by blast
 qed
 
-lemma diff_square: "(x::nat)^2 - y^2 = (x+y)*(x - y)" 
+lemma diff_square: "(x::nat)\<^sup>2 - y\<^sup>2 = (x+y)*(x - y)" 
 proof-
   have "x \<le> y \<or> y \<le> x" by (rule nat_le_linear)
   moreover
   {assume le: "x \<le> y"
-    hence "x ^2 \<le> y^2" by (simp only: numeral_2_eq_2 exp_mono_le Let_def)
+    hence "x\<^sup>2 \<le> y\<^sup>2" by (simp only: numeral_2_eq_2 exp_mono_le Let_def)
     with le have ?thesis by simp }
   moreover
   {assume le: "y \<le> x"
-    hence le2: "y ^2 \<le> x^2" by (simp only: numeral_2_eq_2 exp_mono_le Let_def)
+    hence le2: "y\<^sup>2 \<le> x\<^sup>2" by (simp only: numeral_2_eq_2 exp_mono_le Let_def)
     from le have "\<exists>z. y + z = x" by presburger
     then obtain z where z: "x = y + z" by blast 
-    from le2 have "\<exists>z. x^2 = y^2 + z" by presburger
-    then obtain z2 where z2: "x^2 = y^2 + z2"  by blast
-    from z z2 have ?thesis apply simp by algebra }
+    from le2 have "\<exists>z. x\<^sup>2 = y\<^sup>2 + z" by presburger
+    then obtain z2 where z2: "x\<^sup>2 = y\<^sup>2 + z2" by blast
+    from z z2 have ?thesis by simp algebra }
   ultimately show ?thesis by blast  
 qed
 
@@ -544,29 +544,29 @@
   from g(2,3) dvd_trans[OF p(2)] p(1) show ?thesis by auto
 qed
 lemma coprime_sos: assumes xy: "coprime x y" 
-  shows "coprime (x * y) (x^2 + y^2)"
+  shows "coprime (x * y) (x\<^sup>2 + y\<^sup>2)"
 proof-
-  {assume c: "\<not> coprime (x * y) (x^2 + y^2)"
+  {assume c: "\<not> coprime (x * y) (x\<^sup>2 + y\<^sup>2)"
     from coprime_prime_dvd_ex[OF c] obtain p 
-      where p: "prime p" "p dvd x*y" "p dvd x^2 + y^2" by blast
+      where p: "prime p" "p dvd x*y" "p dvd x\<^sup>2 + y\<^sup>2" by blast
     {assume px: "p dvd x"
       from dvd_mult[OF px, of x] p(3) 
-        obtain r s where "x * x = p * r" and "x^2 + y^2 = p * s"
+        obtain r s where "x * x = p * r" and "x\<^sup>2 + y\<^sup>2 = p * s"
           by (auto elim!: dvdE)
-        then have "y^2 = p * (s - r)" 
+        then have "y\<^sup>2 = p * (s - r)" 
           by (auto simp add: power2_eq_square diff_mult_distrib2)
-        then have "p dvd y^2" ..
+        then have "p dvd y\<^sup>2" ..
       with prime_divexp[OF p(1), of y 2] have py: "p dvd y" .
       from p(1) px py xy[unfolded coprime, rule_format, of p] prime_1  
       have False by simp }
     moreover
     {assume py: "p dvd y"
       from dvd_mult[OF py, of y] p(3)
-        obtain r s where "y * y = p * r" and "x^2 + y^2 = p * s"
+        obtain r s where "y * y = p * r" and "x\<^sup>2 + y\<^sup>2 = p * s"
           by (auto elim!: dvdE)
-        then have "x^2 = p * (s - r)" 
+        then have "x\<^sup>2 = p * (s - r)" 
           by (auto simp add: power2_eq_square diff_mult_distrib2)
-        then have "p dvd x^2" ..
+        then have "p dvd x\<^sup>2" ..
       with prime_divexp[OF p(1), of x 2] have px: "p dvd x" .
       from p(1) px py xy[unfolded coprime, rule_format, of p] prime_1  
       have False by simp }
diff -r 47c9aff07725 -r a1b3784f8129 src/HOL/Old_Number_Theory/Residues.thy
--- a/src/HOL/Old_Number_Theory/Residues.thy	Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/Old_Number_Theory/Residues.thy	Sun Aug 18 19:59:19 2013 +0200
@@ -19,7 +19,7 @@
   where "StandardRes m x = x mod m"
 
 definition QuadRes :: "int => int => bool"
-  where "QuadRes m x = (\<exists>y. ([(y ^ 2) = x] (mod m)))"
+  where "QuadRes m x = (\<exists>y. ([y\<^sup>2 = x] (mod m)))"
 
 definition Legendre :: "int => int => int" where
   "Legendre a p = (if ([a = 0] (mod p)) then 0
diff -r 47c9aff07725 -r a1b3784f8129 src/HOL/Probability/Distributions.thy
--- a/src/HOL/Probability/Distributions.thy	Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/Probability/Distributions.thy	Sun Aug 18 19:59:19 2013 +0200
@@ -372,7 +372,7 @@
   also have "(\<integral> x. (x / measure lborel {a .. b}) * indicator {a .. b} x \<partial>lborel) = (a + b) / 2"
   proof (subst integral_FTC_atLeastAtMost)
     fix x
-    show "DERIV (\<lambda>x. x ^ 2 / (2 * measure lborel {a..b})) x :> x / measure lborel {a..b}"
+    show "DERIV (\<lambda>x. x\<^sup>2 / (2 * measure lborel {a..b})) x :> x / measure lborel {a..b}"
       using uniform_distributed_params[OF D]
       by (auto intro!: DERIV_intros)
     show "isCont (\<lambda>x. x / Sigma_Algebra.measure lborel {a..b}) x"
diff -r 47c9aff07725 -r a1b3784f8129 src/HOL/ex/Groebner_Examples.thy
--- a/src/HOL/ex/Groebner_Examples.thy	Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/ex/Groebner_Examples.thy	Sun Aug 18 19:59:19 2013 +0200
@@ -47,8 +47,8 @@
   by simp
 
 lemma
-  assumes "a * x^2 + b * x + c = (0::int)" and "d * x^2 + e * x + f = 0"
-  shows "d^2*c^2 - 2*d*c*a*f + a^2*f^2 - e*d*b*c - e*b*a*f + a*e^2*c + f*d*b^2 = 0"
+  assumes "a * x\<^sup>2 + b * x + c = (0::int)" and "d * x\<^sup>2 + e * x + f = 0"
+  shows "d\<^sup>2*c\<^sup>2 - 2*d*c*a*f + a\<^sup>2 * f\<^sup>2 - e*d*b*c - e*b*a*f + a*e\<^sup>2*c + f*d*b\<^sup>2 = 0"
   using assms by algebra
 
 lemma "(x::int)^3  - x^2  - 5*x - 3 = 0 \<longleftrightarrow> (x = 3 \<or> x = -1)"
@@ -58,8 +58,8 @@
   by algebra
 
 lemma
-  fixes x::"'a::{idom}"
-  shows "x^2*y = x^2 & x*y^2 = y^2 \<longleftrightarrow>  x=1 & y=1 | x=0 & y=0"
+  fixes x::"'a::idom"
+  shows "x\<^sup>2*y = x\<^sup>2 & x*y\<^sup>2 = y\<^sup>2 \<longleftrightarrow>  x = 1 & y = 1 | x = 0 & y = 0"
   by algebra
 
 subsection {* Lemmas for Lagrange's theorem *}