src/HOL/Decision_Procs/Approximation.thy
2010-12-02 wenzelm 2010-12-02 proper theory name (cf. e84f82418e09);
2010-12-02 hoelzl 2010-12-02 Use coercions in Approximation (by Dmitriy Traytel).
2010-09-20 wenzelm 2010-09-20 more antiquotations;
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-26 haftmann 2010-08-26 formerly unnamed infix impliciation now named HOL.implies
2010-08-25 wenzelm 2010-08-25 approximation_oracle: actually match true/false in ML, not arbitrary values;
2010-08-19 haftmann 2010-08-19 tuned quotes
2010-08-19 haftmann 2010-08-19 use antiquotations for remaining unqualified constants in HOL
2010-07-19 haftmann 2010-07-19 diff_minus subsumes diff_def
2010-07-01 haftmann 2010-07-01 qualified constants Set.member and Set.Collect
2010-06-14 haftmann 2010-06-14 removed simplifier congruence rule of "prod_case"
2010-06-10 haftmann 2010-06-10 tuned quotes, antiquotations and whitespace
2010-05-19 haftmann 2010-05-19 spelt out normalizer explicitly -- avoid dynamic reference to code generator configuration; avoid using old Codegen.eval_term
2010-05-17 wenzelm 2010-05-17 prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;
2010-05-09 huffman 2010-05-09 avoid using real-specific versions of generic lemmas
2010-04-29 haftmann 2010-04-29 code_reflect: specify module name directly after keyword
2010-04-28 haftmann 2010-04-28 use code_reflect
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-02-23 huffman 2010-02-23 adapt to new realpow rules
2010-02-10 haftmann 2010-02-10 rely less on ordered rewriting
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2009-10-20 wenzelm 2009-10-20 tuned;
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-10-13 hoelzl 2009-10-13 order conjunctions to be printed without parentheses
2009-10-13 hoelzl 2009-10-13 approximation now fails earlier when using interval splitting; value [approximate] now supports bounded variables; renamed Var -> Atom for better readability
2009-09-23 hoelzl 2009-09-23 correct variable order in approximate-method
2009-09-22 haftmann 2009-09-22 be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
2009-08-28 nipkow 2009-08-28 tuned proofs
2009-07-30 wenzelm 2009-07-30 qualified Subgoal.FOCUS;
2009-07-26 wenzelm 2009-07-26 replaced old METAHYPS by FOCUS;
2009-06-30 hoelzl 2009-06-30 use DERIV_intros
2009-06-29 hoelzl 2009-06-29 Implemented taylor series expansion for approximation
2009-06-25 hoelzl 2009-06-25 Improved computation of bounds and implemented interval splitting for 'approximation'.
2009-06-08 hoelzl 2009-06-08 Added new evaluator "approximate"
2009-06-15 hoelzl 2009-06-15 tuned
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