
diff -r 638bbd5a4a3b -r 667b5ea637dd src/HOL/ex/Classpackage.thy
--- a/src/HOL/ex/Classpackage.thy	Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/ex/Classpackage.thy	Sat Apr 08 22:51:06 2006 +0200
@@ -150,7 +150,7 @@
 
 abbreviation (in monoid)
   abbrev_npow :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75)
-    "(x \<^loc>\<up> n) = npow n x"
+  "x \<^loc>\<up> n == npow n x"
 
 lemma (in monoid) npow_def:
   "x \<^loc>\<up> 0 = \<^loc>\<one>"
@@ -290,7 +290,7 @@
 
 abbreviation (in group)
   abbrev_pow :: "'a \<Rightarrow> int \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75)
-    "(x \<^loc>\<up> k) = pow k x"
+  "x \<^loc>\<up> k == pow k x"
 
 lemma (in group) int_pow_zero:
   "x \<^loc>\<up> (0::int) = \<^loc>\<one>"




