src/HOL/Power.thy
changeset 7843 077d305615df
parent 5183 89f162de39cf
child 8844 db71c334e854
     1.1 --- a/src/HOL/Power.thy	Wed Oct 13 12:07:03 1999 +0200
     1.2 +++ b/src/HOL/Power.thy	Wed Oct 13 12:07:23 1999 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  
     1.5  Power = Divides + 
     1.6  consts
     1.7 -  binomial :: "[nat,nat] => nat"      ("'(_ choose _')" [50,50])
     1.8 +  binomial :: "[nat,nat] => nat"      (infixl "choose" 65)
     1.9  
    1.10  primrec
    1.11    "p ^ 0 = 1"