choose just as an infix
authorpaulson
Wed Oct 13 12:07:23 1999 +0200 (1999-10-13)
changeset 7843077d305615df
parent 7842 6858c98385c3
child 7844 6462cb4dfdc2
choose just as an infix
src/HOL/Power.thy
     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"