src/Tools/float.ML
Sat, 28 Feb 2009 14:09:58 +0100 wenzelm removed Ids;
Tue, 18 Sep 2007 16:08:00 +0200 wenzelm simplified type int (eliminated IntInf.int, integer);
less more (0) -2 tip