src/HOL/Power.thy
changeset 61955 e96292f32c3c
parent 61944 5d06ecfdb472
child 62083 7582b39f51ed
     1.1 --- a/src/HOL/Power.thy	Mon Dec 28 19:23:15 2015 +0100
     1.2 +++ b/src/HOL/Power.thy	Mon Dec 28 21:47:32 2015 +0100
     1.3 @@ -27,21 +27,17 @@
     1.4  class power = one + times
     1.5  begin
     1.6  
     1.7 -primrec power :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixr "^" 80) where
     1.8 -    power_0: "a ^ 0 = 1"
     1.9 -  | power_Suc: "a ^ Suc n = a * a ^ n"
    1.10 +primrec power :: "'a \<Rightarrow> nat \<Rightarrow> 'a"  (infixr "^" 80)
    1.11 +where
    1.12 +  power_0: "a ^ 0 = 1"
    1.13 +| power_Suc: "a ^ Suc n = a * a ^ n"
    1.14  
    1.15  notation (latex output)
    1.16    power ("(_\<^bsup>_\<^esup>)" [1000] 1000)
    1.17  
    1.18  text \<open>Special syntax for squares.\<close>
    1.19 -
    1.20 -abbreviation (xsymbols)
    1.21 -  power2 :: "'a \<Rightarrow> 'a"  ("(_\<^sup>2)" [1000] 999) where
    1.22 -  "x\<^sup>2 \<equiv> x ^ 2"
    1.23 -
    1.24 -notation (latex output)
    1.25 -  power2  ("(_\<^sup>2)" [1000] 999)
    1.26 +abbreviation power2 :: "'a \<Rightarrow> 'a"  ("(_\<^sup>2)" [1000] 999)
    1.27 +  where "x\<^sup>2 \<equiv> x ^ 2"
    1.28  
    1.29  end
    1.30