# HG changeset patch
# User paulson
# Date 939809243 -7200
# Node ID 077d305615df32f2a9a1bc077b7b890609de7b72
# Parent  6858c98385c3392c3c8c58d6aea9baddd0697fb8
choose just as an infix

diff -r 6858c98385c3 -r 077d305615df src/HOL/Power.thy
--- a/src/HOL/Power.thy	Wed Oct 13 12:07:03 1999 +0200
+++ b/src/HOL/Power.thy	Wed Oct 13 12:07:23 1999 +0200
@@ -9,7 +9,7 @@
 
 Power = Divides + 
 consts
-  binomial :: "[nat,nat] => nat"      ("'(_ choose _')" [50,50])
+  binomial :: "[nat,nat] => nat"      (infixl "choose" 65)
 
 primrec
   "p ^ 0 = 1"