src/HOL/Decision_Procs/Approximation.thy
2013-03-26 wenzelm tuned session specification;
2013-02-15 haftmann two target language numeral types: integer and natural, as replacement for code_numeral;
2012-10-19 webertj Renamed {left,right}_distrib to distrib_{right,left}.
2012-09-13 wenzelm tuned proofs;
2012-04-20 hoelzl hide code generation facts in the Float theory, they are only exported for Approximation
2012-04-19 hoelzl use real :: float => real as lifting-morphism so we can directlry use the rep_eq theorems
2012-04-18 hoelzl use lifting to introduce floating point numbers
2012-04-18 hoelzl replace the float datatype by a type with unique representation
2012-03-25 huffman merged fork with new numeral representation (see NEWS)
2012-02-12 haftmann tuned
2011-11-13 huffman remove lemma float_remove_real_numeral, which duplicated Float.float_number_of
2011-10-12 wenzelm tuned proofs -- eliminated vacuous "induct arbitrary: ..." situations;
2011-09-07 huffman avoid using legacy theorem names
2011-08-28 huffman discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
2011-08-20 huffman remove redundant lemma real_0_le_divide_iff in favor or zero_le_divide_iff
2011-08-19 huffman fold definitions of sin_coeff and cos_coeff in Maclaurin lemmas
2011-08-19 huffman remove some redundant simp rules
2011-04-16 wenzelm modernized structure Proof_Context;
2010-12-29 wenzelm explicit file specifications -- avoid secondary load path;
2010-12-06 hoelzl move coercions to appropriate places
2010-12-06 nipkow moved coercion decl. for int
2010-12-02 wenzelm proper theory name (cf. e84f82418e09);
2010-12-02 hoelzl Use coercions in Approximation (by Dmitriy Traytel).
2010-09-20 wenzelm more antiquotations;
2010-08-28 haftmann formerly unnamed infix equality now named HOL.eq
2010-08-26 haftmann formerly unnamed infix impliciation now named HOL.implies
2010-08-25 wenzelm approximation_oracle: actually match true/false in ML, not arbitrary values;
2010-08-19 haftmann tuned quotes
2010-08-19 haftmann use antiquotations for remaining unqualified constants in HOL
2010-07-19 haftmann diff_minus subsumes diff_def
2010-07-01 haftmann qualified constants Set.member and Set.Collect
2010-06-14 haftmann removed simplifier congruence rule of "prod_case"
2010-06-10 haftmann tuned quotes, antiquotations and whitespace
2010-05-19 haftmann spelt out normalizer explicitly -- avoid dynamic reference to code generator configuration; avoid using old Codegen.eval_term
2010-05-17 wenzelm prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
2010-05-10 huffman avoid using real-specific versions of generic lemmas
2010-04-29 haftmann code_reflect: specify module name directly after keyword
2010-04-28 haftmann use code_reflect
2010-03-20 wenzelm renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-02-23 huffman adapt to new realpow rules
2010-02-10 haftmann rely less on ordered rewriting
2010-02-05 haftmann more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2009-10-20 wenzelm tuned;
2009-10-17 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
2009-10-13 hoelzl order conjunctions to be printed without parentheses
2009-10-13 hoelzl approximation now fails earlier when using interval splitting; value [approximate] now supports bounded variables; renamed Var -> Atom for better readability
2009-09-23 hoelzl correct variable order in approximate-method
2009-09-22 haftmann 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 tuned proofs
2009-07-30 wenzelm qualified Subgoal.FOCUS;
2009-07-26 wenzelm replaced old METAHYPS by FOCUS;
2009-06-30 hoelzl use DERIV_intros
2009-06-29 hoelzl Implemented taylor series expansion for approximation
2009-06-25 hoelzl Improved computation of bounds and implemented interval splitting for 'approximation'.
2009-06-08 hoelzl Added new evaluator "approximate"
2009-06-15 hoelzl tuned
2009-06-24 nipkow corrected and unified thm names
2009-06-08 hoelzl Better approximation of cos around pi.
2009-06-05 hoelzl Approximation: Corrected precision of ln on all real values
2009-06-04 hoelzl Approximation: Implemented argument reduction for cosine. Sinus is now implemented in terms of cosine. Sqrt computes on the entire real numbers
less more (0) -60 tip