src/HOL/ex/Classpackage.thy
changeset 19363 667b5ea637dd
parent 19345 73439b467e75
child 19888 2b4c09941e04
     1.1 --- a/src/HOL/ex/Classpackage.thy	Sat Apr 08 22:12:02 2006 +0200
     1.2 +++ b/src/HOL/ex/Classpackage.thy	Sat Apr 08 22:51:06 2006 +0200
     1.3 @@ -150,7 +150,7 @@
     1.4  
     1.5  abbreviation (in monoid)
     1.6    abbrev_npow :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75)
     1.7 -    "(x \<^loc>\<up> n) = npow n x"
     1.8 +  "x \<^loc>\<up> n == npow n x"
     1.9  
    1.10  lemma (in monoid) npow_def:
    1.11    "x \<^loc>\<up> 0 = \<^loc>\<one>"
    1.12 @@ -290,7 +290,7 @@
    1.13  
    1.14  abbreviation (in group)
    1.15    abbrev_pow :: "'a \<Rightarrow> int \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75)
    1.16 -    "(x \<^loc>\<up> k) = pow k x"
    1.17 +  "x \<^loc>\<up> k == pow k x"
    1.18  
    1.19  lemma (in group) int_pow_zero:
    1.20    "x \<^loc>\<up> (0::int) = \<^loc>\<one>"