diff -r bb18eed53ed6 -r a1119cf551e8 src/HOL/Multivariate_Analysis/L2_Norm.thy
--- a/src/HOL/Multivariate_Analysis/L2_Norm.thy	Tue Aug 13 14:20:22 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/L2_Norm.thy	Tue Aug 13 16:25:47 2013 +0200
@@ -9,7 +9,7 @@
 begin
 
 definition
-  "setL2 f A = sqrt (\<Sum>i\<in>A. (f i)\<twosuperior>)"
+  "setL2 f A = sqrt (\<Sum>i\<in>A. (f i)\<^sup>2)"
 
 lemma setL2_cong:
   "\<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setL2 f A = setL2 g B"
@@ -27,7 +27,7 @@
 
 lemma setL2_insert [simp]:
   "\<lbrakk>finite F; a \<notin> F\<rbrakk> \<Longrightarrow>
-    setL2 f (insert a F) = sqrt ((f a)\<twosuperior> + (setL2 f F)\<twosuperior>)"
+    setL2 f (insert a F) = sqrt ((f a)\<^sup>2 + (setL2 f F)\<^sup>2)"
   unfolding setL2_def by (simp add: setsum_nonneg)
 
 lemma setL2_nonneg [simp]: "0 \<le> setL2 f A"
@@ -94,12 +94,12 @@
     show ?case by simp
   next
     case (insert x F)
-    hence "sqrt ((f x + g x)\<twosuperior> + (setL2 (\<lambda>i. f i + g i) F)\<twosuperior>) \<le>
-           sqrt ((f x + g x)\<twosuperior> + (setL2 f F + setL2 g F)\<twosuperior>)"
+    hence "sqrt ((f x + g x)\<^sup>2 + (setL2 (\<lambda>i. f i + g i) F)\<^sup>2) \<le>
+           sqrt ((f x + g x)\<^sup>2 + (setL2 f F + setL2 g F)\<^sup>2)"
       by (intro real_sqrt_le_mono add_left_mono power_mono insert
                 setL2_nonneg add_increasing zero_le_power2)
     also have
-      "\<dots> \<le> sqrt ((f x)\<twosuperior> + (setL2 f F)\<twosuperior>) + sqrt ((g x)\<twosuperior> + (setL2 g F)\<twosuperior>)"
+      "\<dots> \<le> sqrt ((f x)\<^sup>2 + (setL2 f F)\<^sup>2) + sqrt ((g x)\<^sup>2 + (setL2 g F)\<^sup>2)"
       by (rule real_sqrt_sum_squares_triangle_ineq)
     finally show ?case
       using insert by simp
@@ -107,7 +107,7 @@
 qed
 
 lemma sqrt_sum_squares_le_sum:
-  "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> sqrt (x\<twosuperior> + y\<twosuperior>) \<le> x + y"
+  "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> sqrt (x\<^sup>2 + y\<^sup>2) \<le> x + y"
   apply (rule power2_le_imp_le)
   apply (simp add: power2_sum mult_nonneg_nonneg)
   apply simp
@@ -125,7 +125,7 @@
   apply simp
   done
 
-lemma sqrt_sum_squares_le_sum_abs: "sqrt (x\<twosuperior> + y\<twosuperior>) \<le> \<bar>x\<bar> + \<bar>y\<bar>"
+lemma sqrt_sum_squares_le_sum_abs: "sqrt (x\<^sup>2 + y\<^sup>2) \<le> \<bar>x\<bar> + \<bar>y\<bar>"
   apply (rule power2_le_imp_le)
   apply (simp add: power2_sum mult_nonneg_nonneg)
   apply simp
@@ -143,14 +143,14 @@
 
 lemma setL2_mult_ineq_lemma:
   fixes a b c d :: real
-  shows "2 * (a * c) * (b * d) \<le> a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior>"
+  shows "2 * (a * c) * (b * d) \<le> a\<^sup>2 * d\<^sup>2 + b\<^sup>2 * c\<^sup>2"
 proof -
-  have "0 \<le> (a * d - b * c)\<twosuperior>" by simp
-  also have "\<dots> = a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior> - 2 * (a * d) * (b * c)"
+  have "0 \<le> (a * d - b * c)\<^sup>2" by simp
+  also have "\<dots> = a\<^sup>2 * d\<^sup>2 + b\<^sup>2 * c\<^sup>2 - 2 * (a * d) * (b * c)"
     by (simp only: power2_diff power_mult_distrib)
-  also have "\<dots> = a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior> - 2 * (a * c) * (b * d)"
+  also have "\<dots> = a\<^sup>2 * d\<^sup>2 + b\<^sup>2 * c\<^sup>2 - 2 * (a * c) * (b * d)"
     by simp
-  finally show "2 * (a * c) * (b * d) \<le> a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior>"
+  finally show "2 * (a * c) * (b * d) \<le> a\<^sup>2 * d\<^sup>2 + b\<^sup>2 * c\<^sup>2"
     by simp
 qed