changeset 5183 | 89f162de39cf |
parent 4628 | 0c7e97836e3c |
child 7843 | 077d305615df |
--- a/src/HOL/Power.thy Fri Jul 24 13:02:01 1998 +0200 +++ b/src/HOL/Power.thy Fri Jul 24 13:03:20 1998 +0200 @@ -11,11 +11,11 @@ consts binomial :: "[nat,nat] => nat" ("'(_ choose _')" [50,50]) -primrec "op ^" nat +primrec "p ^ 0 = 1" "p ^ (Suc n) = (p::nat) * (p ^ n)" -primrec "binomial" nat +primrec binomial_0 "(0 choose k) = (if k = 0 then 1 else 0)" binomial_Suc "(Suc n choose k) =