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 \ nat \ 'a" (infix "\<^loc>\" 75) - "(x \<^loc>\ n) = npow n x" + "x \<^loc>\ n == npow n x" lemma (in monoid) npow_def: "x \<^loc>\ 0 = \<^loc>\" @@ -290,7 +290,7 @@ abbreviation (in group) abbrev_pow :: "'a \ int \ 'a" (infix "\<^loc>\" 75) - "(x \<^loc>\ k) = pow k x" + "x \<^loc>\ k == pow k x" lemma (in group) int_pow_zero: "x \<^loc>\ (0::int) = \<^loc>\"