src/HOL/Power.thy
changeset 4628 0c7e97836e3c
parent 3390 0c7625196d95
child 5183 89f162de39cf
equal deleted inserted replaced
4627:ae95666c71cc 4628:0c7e97836e3c
    17   
    17   
    18 primrec "binomial" nat
    18 primrec "binomial" nat
    19   binomial_0   "(0     choose k) = (if k = 0 then 1 else 0)"
    19   binomial_0   "(0     choose k) = (if k = 0 then 1 else 0)"
    20 
    20 
    21   binomial_Suc "(Suc n choose k) =
    21   binomial_Suc "(Suc n choose k) =
    22                 (if k = 0 then 1 else (n choose pred k) + (n choose k))"
    22                 (if k = 0 then 1 else (n choose (k - 1)) + (n choose k))"
    23 
    23 
    24 end
    24 end
    25 
    25