src/HOL/Real/Float.thy
2008-06-26 haftmann 2008-06-26 dropped recdef
2008-03-17 wenzelm 2008-03-17 avoid rebinding of existing facts; removed duplicate lemmas;
2008-02-17 huffman 2008-02-17 New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
2008-02-16 huffman 2008-02-16 added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
2007-09-20 obua 2007-09-20 changed lemmas
2007-08-17 obua 2007-08-17 changed floatarith lemmas
2007-08-02 wenzelm 2007-08-02 turned simp_depth_limit into configuration option;
2007-06-23 nipkow 2007-06-23 tuned and renamed group_eq_simps and ring_eq_simps
2007-06-20 huffman 2007-06-20 change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
2007-06-13 huffman 2007-06-13 removed constant int :: nat => int; int is now an abbreviation for of_nat :: nat => int
2007-06-11 chaieb 2007-06-11 tuned Proof
2007-06-05 haftmann 2007-06-05 moved generic algebra modules
2007-05-14 haftmann 2007-05-14 reorganized float arithmetic
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