src/HOL/Power.thy
changeset 7843 077d305615df
parent 5183 89f162de39cf
child 8844 db71c334e854
equal deleted inserted replaced
7842:6858c98385c3 7843:077d305615df
     7 Also binomial coefficents
     7 Also binomial coefficents
     8 *)
     8 *)
     9 
     9 
    10 Power = Divides + 
    10 Power = Divides + 
    11 consts
    11 consts
    12   binomial :: "[nat,nat] => nat"      ("'(_ choose _')" [50,50])
    12   binomial :: "[nat,nat] => nat"      (infixl "choose" 65)
    13 
    13 
    14 primrec
    14 primrec
    15   "p ^ 0 = 1"
    15   "p ^ 0 = 1"
    16   "p ^ (Suc n) = (p::nat) * (p ^ n)"
    16   "p ^ (Suc n) = (p::nat) * (p ^ n)"
    17   
    17