# HG changeset patch
# User chaieb
# Date 1180949959 -7200
# Node ID 861ab9c18e1818f80009eca5e40fed83714661df
# Parent  aef7b4e5c8fe1256b817ba3705335988426b6803
removed fixmes

diff -r aef7b4e5c8fe -r 861ab9c18e18 src/Pure/General/rat.ML
--- 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;