removed fixmes
authorchaieb
Mon, 04 Jun 2007 11:39:19 +0200
changeset 23232 861ab9c18e18
parent 23231 aef7b4e5c8fe
child 23233 76462538f349
removed fixmes
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;