src/HOL/Decision_Procs/Approximation.thy
2009-06-24 nipkow 2009-06-24 corrected and unified thm names
2009-06-08 hoelzl 2009-06-08 Better approximation of cos around pi.
2009-06-05 hoelzl 2009-06-05 Approximation: Corrected precision of ln on all real values
2009-06-04 hoelzl 2009-06-04 Approximation: Implemented argument reduction for cosine. Sinus is now implemented in terms of cosine. Sqrt computes on the entire real numbers
2009-05-14 nipkow 2009-05-14 Cleaned up Parity a little
2009-05-05 hoelzl 2009-05-05 optimized Approximation by precompiling approx_inequality
2009-04-29 hoelzl 2009-04-29 replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
2009-04-24 haftmann 2009-04-24 funpow and relpow with shared "^^" syntax
2009-04-23 haftmann 2009-04-23 adaptions due to rearrangment of power operation
2009-04-20 haftmann 2009-04-20 power operation on functions with syntax o^; power operation on relations with syntax ^^
2009-04-08 wenzelm 2009-04-08 updated official title of contribution by Johannes Hoelzl;
2009-03-16 wenzelm 2009-03-16 simplified method setup;
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
2009-03-11 hoelzl 2009-03-11 Extended approximation boundaries by fractions and base-2 floating point numbers
2009-03-11 hoelzl 2009-03-11 Updated paths in Decision_Procs comments and NEWS
2009-03-10 hoelzl 2009-03-10 Fixed type error which appeared when Approximation bounds where specified as floating point numbers
2009-03-04 huffman 2009-03-04 declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
2009-02-26 wenzelm 2009-02-26 standard headers; eliminated non-ASCII chars, which are fragile in the age of unicode;
2009-02-06 haftmann 2009-02-06 session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there