src/HOL/Real/Float.ML
Wed, 06 Sep 2006 13:48:02 +0200 haftmann got rid of Numeral.bin type
Fri, 17 Mar 2006 09:34:23 +0100 haftmann renamed op < <= to Orderings.less(_eq)
Fri, 10 Mar 2006 15:33:48 +0100 haftmann renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
Tue, 19 Jul 2005 16:16:53 +0200 obua proving bounds for real linear programs
Thu, 14 Jul 2005 17:21:35 +0200 wenzelm tuned;
Tue, 12 Jul 2005 21:49:38 +0200 obua - use TableFun instead of homebrew binary tree in am_interpreter.ML
less more (0) tip