src/HOL/Library/Float.thy
2010-05-09 ago avoid using real-specific versions of generic lemmas
2010-02-23 ago moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power
2010-02-08 ago separate library theory for type classes combining lattices with various algebraic structures
2009-11-10 ago eliminated some old uses of cumulative prems (!) in proof methods;
2009-10-17 ago eliminated hard tabulators, guessing at each author's individual tab-width;
2009-07-14 ago prefer code_inline over code_unfold; use code_unfold_post where appropriate
2009-07-14 ago code attributes use common underscore convention
2009-06-29 ago Implemented taylor series expansion for approximation
2009-06-04 ago Approximation: Implemented argument reduction for cosine. Sinus is now implemented in terms of cosine. Sqrt computes on the entire real numbers
2009-04-29 ago replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
2009-04-29 ago farewell to class recpower
2009-04-22 ago power operation defined generic
2009-03-04 ago Merge.
2009-03-04 ago Merge.
2009-03-01 ago removed redundant lemmas
2009-02-26 ago standard headers;
2009-02-21 ago removed redundant thms
2009-02-18 ago add header
2009-02-05 ago Added new Float theory and moved old Library/Float.thy to ComputeFloat
2009-01-28 ago Replaced group_ and ring_simps by algebra_simps;
2008-12-09 ago move all neg-related lemmas to NatBin; make type of neg specific to int
2008-12-03 ago enable eq_bin_simps for simplifying equalities on numerals
2008-12-03 ago fix proofs related to simplification of inequalities on numerals
2008-12-03 ago made repository layout more coherent with logical distribution structure; stripped some $Id$s