src/HOL/Power.thy
changeset 5183 89f162de39cf
parent 4628 0c7e97836e3c
child 7843 077d305615df
     1.1 --- a/src/HOL/Power.thy	Fri Jul 24 13:02:01 1998 +0200
     1.2 +++ b/src/HOL/Power.thy	Fri Jul 24 13:03:20 1998 +0200
     1.3 @@ -11,11 +11,11 @@
     1.4  consts
     1.5    binomial :: "[nat,nat] => nat"      ("'(_ choose _')" [50,50])
     1.6  
     1.7 -primrec "op ^" nat
     1.8 +primrec
     1.9    "p ^ 0 = 1"
    1.10    "p ^ (Suc n) = (p::nat) * (p ^ n)"
    1.11    
    1.12 -primrec "binomial" nat
    1.13 +primrec
    1.14    binomial_0   "(0     choose k) = (if k = 0 then 1 else 0)"
    1.15  
    1.16    binomial_Suc "(Suc n choose k) =