src/HOL/Power.thy
changeset 8844 db71c334e854
parent 7843 077d305615df
child 14348 744c868ee0b7
     1.1 --- a/src/HOL/Power.thy	Tue May 09 14:16:32 2000 +0200
     1.2 +++ b/src/HOL/Power.thy	Tue May 09 14:33:43 2000 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4  consts
     1.5    binomial :: "[nat,nat] => nat"      (infixl "choose" 65)
     1.6  
     1.7 -primrec
     1.8 +primrec (power)
     1.9    "p ^ 0 = 1"
    1.10    "p ^ (Suc n) = (p::nat) * (p ^ n)"
    1.11