diff -r 250e1da3204b -r af5ef0d4d655 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/Power.thy	Tue Oct 16 23:12:45 2007 +0200
@@ -12,13 +12,13 @@
 begin
 
 class power = type +
-  fixes power :: "'a \<Rightarrow> nat \<Rightarrow> 'a"            (infixr "\<^loc>^" 80)
+  fixes power :: "'a \<Rightarrow> nat \<Rightarrow> 'a"            (infixr "^" 80)
 
 subsection{*Powers for Arbitrary Monoids*}
 
 class recpower = monoid_mult + power +
-  assumes power_0 [simp]: "a \<^loc>^ 0       = \<^loc>1"
-  assumes power_Suc:      "a \<^loc>^ Suc n = a \<^loc>* (a \<^loc>^ n)"
+  assumes power_0 [simp]: "a ^ 0       = 1"
+  assumes power_Suc:      "a ^ Suc n = a * (a ^ n)"
 
 lemma power_0_Suc [simp]: "(0::'a::{recpower,semiring_0}) ^ (Suc n) = 0"
   by (simp add: power_Suc)