src/HOL/Real/Float.thy
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-11-08 wenzelm 2006-11-08 moved theories Parity, GCD, Binomial to Library;
2006-09-28 wenzelm 2006-09-28 proper use of float.ML;
2006-09-26 huffman 2006-09-26 add header
2006-09-06 haftmann 2006-09-06 got rid of Numeral.bin type
2006-07-26 webertj 2006-07-26 linear arithmetic splits certain operators (e.g. min, max, abs)
2006-06-02 wenzelm 2006-06-02 misc cleanup;
2005-07-19 wenzelm 2005-07-19 isatool fixheaders;
2005-07-12 obua 2005-07-12 - use TableFun instead of homebrew binary tree in am_interpreter.ML - add Floats to HOL/Real