author | chaieb |
Mon, 04 Jun 2007 11:39:19 +0200 | |
changeset 23232 | 861ab9c18e18 |
parent 23231 | aef7b4e5c8fe |
child 23233 | 76462538f349 |
--- a/src/Pure/General/rat.ML Mon Jun 04 11:38:34 2007 +0200 +++ b/src/Pure/General/rat.ML Mon Jun 04 11:39:19 2007 +0200 @@ -122,10 +122,10 @@ end; -infix 5 +/; (*FIXME infix 5?*) +infix 5 +/; infix 5 -/; infix 7 */; -infix 7 //; (*FIXME infix 7?*) +infix 7 //; infix 4 =/ </ <=/ >/ >=/ <>/; fun a +/ b = Rat.add a b;