src/HOL/Decision_Procs/Approximation.thy
Mon, 06 Dec 2010 19:54:48 +0100 hoelzl move coercions to appropriate places
Mon, 06 Dec 2010 19:18:02 +0100 nipkow moved coercion decl. for int
Thu, 02 Dec 2010 21:23:56 +0100 wenzelm proper theory name (cf. e84f82418e09);
Thu, 02 Dec 2010 16:16:18 +0100 hoelzl Use coercions in Approximation (by Dmitriy Traytel).
Mon, 20 Sep 2010 15:29:53 +0200 wenzelm more antiquotations;
Sat, 28 Aug 2010 16:14:32 +0200 haftmann formerly unnamed infix equality now named HOL.eq
Thu, 26 Aug 2010 20:51:17 +0200 haftmann formerly unnamed infix impliciation now named HOL.implies
Wed, 25 Aug 2010 18:38:49 +0200 wenzelm approximation_oracle: actually match true/false in ML, not arbitrary values;
Thu, 19 Aug 2010 16:08:59 +0200 haftmann tuned quotes
Thu, 19 Aug 2010 11:02:14 +0200 haftmann use antiquotations for remaining unqualified constants in HOL
Mon, 19 Jul 2010 16:09:44 +0200 haftmann diff_minus subsumes diff_def
Thu, 01 Jul 2010 16:54:42 +0200 haftmann qualified constants Set.member and Set.Collect
Mon, 14 Jun 2010 15:10:36 +0200 haftmann removed simplifier congruence rule of "prod_case"
Thu, 10 Jun 2010 12:24:03 +0200 haftmann tuned quotes, antiquotations and whitespace
Wed, 19 May 2010 12:35:20 +0200 haftmann spelt out normalizer explicitly -- avoid dynamic reference to code generator configuration; avoid using old Codegen.eval_term
Mon, 17 May 2010 23:54:15 +0200 wenzelm prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
Sun, 09 May 2010 22:51:11 -0700 huffman avoid using real-specific versions of generic lemmas
Thu, 29 Apr 2010 15:00:40 +0200 haftmann code_reflect: specify module name directly after keyword
Wed, 28 Apr 2010 21:41:05 +0200 haftmann use code_reflect
Sat, 20 Mar 2010 17:33:11 +0100 wenzelm renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
Tue, 23 Feb 2010 12:35:32 -0800 huffman adapt to new realpow rules
Wed, 10 Feb 2010 08:49:25 +0100 haftmann rely less on ordered rewriting
Fri, 05 Feb 2010 14:33:50 +0100 haftmann more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
Tue, 20 Oct 2009 21:22:37 +0200 wenzelm tuned;
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Tue, 13 Oct 2009 13:40:26 +0200 hoelzl order conjunctions to be printed without parentheses
Tue, 13 Oct 2009 12:02:55 +0200 hoelzl approximation now fails earlier when using interval splitting; value [approximate] now supports bounded variables; renamed Var -> Atom for better readability
Wed, 23 Sep 2009 13:17:17 +0200 hoelzl correct variable order in approximate-method
Tue, 22 Sep 2009 15:36:55 +0200 haftmann be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
Fri, 28 Aug 2009 20:02:18 +0200 nipkow tuned proofs
Thu, 30 Jul 2009 12:20:43 +0200 wenzelm qualified Subgoal.FOCUS;
Sun, 26 Jul 2009 20:38:11 +0200 wenzelm replaced old METAHYPS by FOCUS;
Tue, 30 Jun 2009 18:21:55 +0200 hoelzl use DERIV_intros
Mon, 29 Jun 2009 23:29:11 +0200 hoelzl Implemented taylor series expansion for approximation
Thu, 25 Jun 2009 18:12:40 +0200 hoelzl Improved computation of bounds and implemented interval splitting for 'approximation'.
Mon, 08 Jun 2009 18:37:35 +0200 hoelzl Added new evaluator "approximate"
Mon, 15 Jun 2009 12:14:40 +0200 hoelzl tuned
Wed, 24 Jun 2009 09:41:14 +0200 nipkow corrected and unified thm names
Mon, 08 Jun 2009 18:34:02 +0200 hoelzl Better approximation of cos around pi.
Fri, 05 Jun 2009 17:01:02 +0200 hoelzl Approximation: Corrected precision of ln on all real values
Thu, 04 Jun 2009 17:55:47 +0200 hoelzl Approximation: Implemented argument reduction for cosine. Sinus is now implemented in terms of cosine. Sqrt computes on the entire real numbers
Thu, 14 May 2009 15:39:15 +0200 nipkow Cleaned up Parity a little
Tue, 05 May 2009 17:09:18 +0200 hoelzl optimized Approximation by precompiling approx_inequality
Wed, 29 Apr 2009 20:19:50 +0200 hoelzl replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
Fri, 24 Apr 2009 17:45:15 +0200 haftmann funpow and relpow with shared "^^" syntax
Thu, 23 Apr 2009 12:17:51 +0200 haftmann adaptions due to rearrangment of power operation
Mon, 20 Apr 2009 09:32:07 +0200 haftmann power operation on functions with syntax o^; power operation on relations with syntax ^^
Wed, 08 Apr 2009 16:35:03 +0200 wenzelm updated official title of contribution by Johannes Hoelzl;
Mon, 16 Mar 2009 18:24:30 +0100 wenzelm simplified method setup;
Fri, 13 Mar 2009 19:58:26 +0100 wenzelm unified type Proof.method and pervasive METHOD combinators;
Wed, 11 Mar 2009 13:53:51 +0100 hoelzl Extended approximation boundaries by fractions and base-2 floating point numbers
Wed, 11 Mar 2009 10:58:18 +0100 hoelzl Updated paths in Decision_Procs comments and NEWS
Tue, 10 Mar 2009 16:36:22 +0100 hoelzl Fixed type error which appeared when Approximation bounds where specified as floating point numbers
Wed, 04 Mar 2009 17:12:23 -0800 huffman declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
Thu, 26 Feb 2009 20:56:59 +0100 wenzelm standard headers;
Fri, 06 Feb 2009 15:15:32 +0100 haftmann session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
less more (0) tip