src/HOL/Decision_Procs/Algebra_Aux.thy

 next
   assume "x = y"
   with assms show "x \<ominus> y = \<zero>" by (simp add: minus_eq r_neg)
 qed
 
-lemma power2_eq_square: "x \<in> carrier R \<Longrightarrow> x (^) (2::nat) = x \<otimes> x"
+lemma power2_eq_square: "x \<in> carrier R \<Longrightarrow> x [^] (2::nat) = x \<otimes> x"
   by (simp add: numeral_eq_Suc)
 
 lemma eq_neg_iff_add_eq_0:
   assumes "x \<in> carrier R" "y \<in> carrier R"
   shows "x = \<ominus> y \<longleftrightarrow> x \<oplus> y = \<zero>"

 lemma mult2: "x \<in> carrier R \<Longrightarrow> x \<oplus> x = \<guillemotleft>2\<guillemotright> \<otimes> x"
   by (simp add: of_int_2 l_distr)
 
 end
 
-lemma (in cring) of_int_power [simp]: "\<guillemotleft>i ^ n\<guillemotright> = \<guillemotleft>i\<guillemotright> (^) n"
+lemma (in cring) of_int_power [simp]: "\<guillemotleft>i ^ n\<guillemotright> = \<guillemotleft>i\<guillemotright> [^] n"
   by (induct n) (simp_all add: m_ac)
 
 definition cring_class_ops :: "'a::comm_ring_1 ring"
   where "cring_class_ops \<equiv> \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"
 

   done
 
 lemma minus_class: "x \<ominus>\<^bsub>cring_class_ops\<^esub> y = x - y"
   by (simp add: a_minus_def carrier_class plus_class uminus_class)
 
-lemma power_class: "x (^)\<^bsub>cring_class_ops\<^esub> n = x ^ n"
+lemma power_class: "x [^]\<^bsub>cring_class_ops\<^esub> n = x ^ n"
   by (induct n) (simp_all add: one_class times_class
     monoid.nat_pow_0 [OF comm_monoid.axioms(1) [OF cring.axioms(2) [OF cring_class]]]
     monoid.nat_pow_Suc [OF comm_monoid.axioms(1) [OF cring.axioms(2) [OF cring_class]]])
 
 lemma of_nat_class: "\<guillemotleft>n\<guillemotright>\<^sub>\<nat>\<^bsub>cring_class_ops\<^esub> = of_nat n"

     and "(\<one>\<^bsub>cring_class_ops\<^esub>::'a) = 1"
     and "(x::'a) \<oplus>\<^bsub>cring_class_ops\<^esub> y = x + y"
     and "(x::'a) \<otimes>\<^bsub>cring_class_ops\<^esub> y = x * y"
     and "\<ominus>\<^bsub>cring_class_ops\<^esub> (x::'a) = - x"
     and "(x::'a) \<ominus>\<^bsub>cring_class_ops\<^esub> y = x - y"
-    and "(x::'a) (^)\<^bsub>cring_class_ops\<^esub> n = x ^ n"
+    and "(x::'a) [^]\<^bsub>cring_class_ops\<^esub> n = x ^ n"
     and "\<guillemotleft>n\<guillemotright>\<^sub>\<nat>\<^bsub>cring_class_ops\<^esub> = of_nat n"
     and "((\<guillemotleft>i\<guillemotright>\<^bsub>cring_class_ops\<^esub>)::'a) = of_int i"
     and "(Int.of_int (numeral m)::'a) = numeral m"
   by (simp_all add: cring_class class_simps)
 
 lemma (in domain) nat_pow_eq_0_iff [simp]:
-  "a \<in> carrier R \<Longrightarrow> (a (^) (n::nat) = \<zero>) = (a = \<zero> \<and> n \<noteq> 0)"
+  "a \<in> carrier R \<Longrightarrow> (a [^] (n::nat) = \<zero>) = (a = \<zero> \<and> n \<noteq> 0)"
   by (induct n) (auto simp add: integral_iff)
 
 lemma (in domain) square_eq_iff:
   assumes "x \<in> carrier R" "y \<in> carrier R"
   shows "(x \<otimes> x = y \<otimes> y) = (x = y \<or> x = \<ominus> y)"

     a \<otimes> (b \<oslash> c) = a \<otimes> b \<oslash> c"
   by (simp add: m_div_def m_ac)
 
 lemma nonzero_power_divide:
   "a \<in> carrier R \<Longrightarrow> b \<in> carrier R \<Longrightarrow> b \<noteq> \<zero> \<Longrightarrow>
-    (a \<oslash> b) (^) (n::nat) = a (^) n \<oslash> b (^) n"
+    (a \<oslash> b) [^] (n::nat) = a [^] n \<oslash> b [^] n"
   by (induct n) (simp_all add: nonzero_divide_divide_eq_left)
 
 lemma r_diff_distr:
   "x \<in> carrier R \<Longrightarrow> y \<in> carrier R \<Longrightarrow> z \<in> carrier R \<Longrightarrow>
     z \<otimes> (x \<ominus> y) = z \<otimes> x \<ominus> z \<otimes> y"

     and "(\<one>\<^bsub>cring_class_ops\<^esub>::'a) = 1"
     and "(x::'a) \<oplus>\<^bsub>cring_class_ops\<^esub> y = x + y"
     and "(x::'a) \<otimes>\<^bsub>cring_class_ops\<^esub> y = x * y"
     and "\<ominus>\<^bsub>cring_class_ops\<^esub> (x::'a) = - x"
     and "(x::'a) \<ominus>\<^bsub>cring_class_ops\<^esub> y = x - y"
-    and "(x::'a) (^)\<^bsub>cring_class_ops\<^esub> n = x ^ n"
+    and "(x::'a) [^]\<^bsub>cring_class_ops\<^esub> n = x ^ n"
     and "\<guillemotleft>n\<guillemotright>\<^sub>\<nat>\<^bsub>cring_class_ops\<^esub> = of_nat n"
     and "((\<guillemotleft>i\<guillemotright>\<^bsub>cring_class_ops\<^esub>)::'a) = of_int i"
     and "(x::'a) \<oslash>\<^bsub>cring_class_ops\<^esub> y = x / y"
     and "(Int.of_int (numeral m)::'a) = numeral m"
   by (simp_all add: field_class class_simps div_class)