src/HOL/Decision_Procs/Approximation.thy
Tue, 07 Jul 2015 00:48:42 +0200 wenzelm tuned proofs;
Sat, 20 Jun 2015 16:31:44 +0200 wenzelm isabelle update_cartouches;
Sat, 11 Apr 2015 11:56:40 +0100 paulson Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
Mon, 30 Mar 2015 10:52:54 +0200 eberlm exposed approximation in ML
Thu, 19 Mar 2015 14:24:51 +0000 paulson New material for complex sin, cos, tan, Ln, also some reorganisation
Wed, 18 Mar 2015 14:13:27 +0000 paulson Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
Mon, 16 Mar 2015 15:30:00 +0000 paulson The factorial function, "fact", now has type "nat => 'a"
Mon, 09 Mar 2015 16:28:19 +0000 paulson sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
Fri, 06 Mar 2015 15:58:56 +0100 wenzelm Thm.cterm_of and Thm.ctyp_of operate on local context;
Wed, 04 Mar 2015 19:53:18 +0100 wenzelm tuned signature -- prefer qualified names;
Tue, 03 Mar 2015 19:08:04 +0100 traytel eliminated some clones of Proof_Context.cterm_of
Tue, 10 Feb 2015 14:48:26 +0100 wenzelm proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2};
Wed, 12 Nov 2014 17:37:43 +0100 immler added quickcheck[approximation]
Wed, 12 Nov 2014 17:37:43 +0100 immler disjunction and conjunction for forms
Wed, 12 Nov 2014 17:37:43 +0100 immler truncate intermediate results in horner to improve performance of approximate;
Wed, 12 Nov 2014 17:36:29 +0100 immler simplified computations based on round_up by reducing to round_down;
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Thu, 30 Oct 2014 21:02:01 +0100 haftmann more simp rules concerning dvd and even/odd
Sun, 19 Oct 2014 18:05:26 +0200 haftmann prefer generic elimination rules for even/odd over specialized unfold rules for nat
Sun, 21 Sep 2014 16:56:11 +0200 haftmann explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
Thu, 11 Sep 2014 19:32:36 +0200 blanchet updated news
Tue, 09 Sep 2014 20:51:36 +0200 blanchet use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
Fri, 04 Jul 2014 20:18:47 +0200 haftmann reduced name variants for assoc and commute on plus and mult
Sat, 28 Jun 2014 09:16:42 +0200 haftmann fact consolidation
Fri, 09 May 2014 08:13:36 +0200 haftmann prefer separate command for approximation
Wed, 07 May 2014 12:25:35 +0200 hoelzl avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
Thu, 01 May 2014 10:20:20 +0200 haftmann separate ML module
Mon, 14 Apr 2014 13:08:17 +0200 hoelzl added divide_nonneg_nonneg and co; made it a simp rule
Sat, 12 Apr 2014 17:26:27 +0200 nipkow made mult_pos_pos a simp rule
Fri, 11 Apr 2014 22:53:33 +0200 nipkow made divide_pos_pos a simp rule
Fri, 11 Apr 2014 13:36:57 +0200 nipkow made mult_nonneg_nonneg a simp rule
Wed, 09 Apr 2014 13:15:21 +0200 hoelzl generalize ln/log_powr; add log_base_powr/pow
Wed, 09 Apr 2014 09:37:47 +0200 hoelzl revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
Fri, 04 Apr 2014 17:58:25 +0100 paulson divide_minus_left divide_minus_right are in field_simps but are not default simprules
Thu, 03 Apr 2014 18:24:08 +0200 hoelzl fix #0556204bc230
Thu, 03 Apr 2014 17:56:08 +0200 hoelzl merged DERIV_intros, has_derivative_intros into derivative_intros
Tue, 18 Mar 2014 11:58:30 -0700 huffman adapt to Isabelle/c726ecfb22b6
Thu, 13 Mar 2014 07:07:07 +0100 nipkow enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions
Sat, 15 Feb 2014 18:48:43 +0100 wenzelm removed dead code;
Fri, 14 Feb 2014 07:53:46 +0100 blanchet merged 'Option.map' and 'Option.map_option'
Wed, 12 Feb 2014 08:35:57 +0100 blanchet renamed '{prod,sum,bool,unit}_case' to 'case_...'
Wed, 12 Feb 2014 08:35:56 +0100 blanchet adapted theories to '{case,rec}_{list,option}' names
Mon, 16 Dec 2013 17:08:22 +0100 immler additional definitions and lemmas for Float
Tue, 19 Nov 2013 10:05:53 +0100 haftmann eliminiated neg_numeral in favour of - (numeral _)
Tue, 05 Nov 2013 15:10:59 +0100 hoelzl tuned proofs in Approximation
Fri, 01 Nov 2013 18:51:14 +0100 haftmann more simplification rules on unary and binary minus
Sun, 18 Aug 2013 19:59:19 +0200 wenzelm more symbols;
Sun, 02 Jun 2013 07:46:40 +0200 haftmann make reification part of HOL
Fri, 31 May 2013 09:30:32 +0200 haftmann decomposed reflection steps into conversions;
Fri, 31 May 2013 09:30:32 +0200 haftmann dropped vacuous prefix
Fri, 24 May 2013 17:00:46 +0200 wenzelm tuned signature;
Mon, 20 May 2013 20:47:33 +0200 wenzelm proper context;
Sun, 21 Apr 2013 10:41:18 +0200 haftmann combined reify_data.ML into reflection.ML;
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Tue, 26 Mar 2013 20:37:32 +0100 wenzelm tuned session specification;
Fri, 15 Feb 2013 08:31:31 +0100 haftmann two target language numeral types: integer and natural, as replacement for code_numeral;
Fri, 19 Oct 2012 15:12:52 +0200 webertj Renamed {left,right}_distrib to distrib_{right,left}.
Thu, 13 Sep 2012 17:20:04 +0200 wenzelm tuned proofs;
Fri, 20 Apr 2012 11:14:39 +0200 hoelzl hide code generation facts in the Float theory, they are only exported for Approximation
Thu, 19 Apr 2012 11:55:30 +0200 hoelzl use real :: float => real as lifting-morphism so we can directlry use the rep_eq theorems
Wed, 18 Apr 2012 14:29:22 +0200 hoelzl use lifting to introduce floating point numbers
Wed, 18 Apr 2012 14:29:21 +0200 hoelzl replace the float datatype by a type with unique representation
Sun, 25 Mar 2012 20:15:39 +0200 huffman merged fork with new numeral representation (see NEWS)
Sun, 12 Feb 2012 22:10:05 +0100 haftmann tuned
Sun, 13 Nov 2011 19:30:35 +0100 huffman remove lemma float_remove_real_numeral, which duplicated Float.float_number_of
Wed, 12 Oct 2011 20:16:48 +0200 wenzelm tuned proofs -- eliminated vacuous "induct arbitrary: ..." situations;
Wed, 07 Sep 2011 09:02:58 -0700 huffman avoid using legacy theorem names
Sun, 28 Aug 2011 09:20:12 -0700 huffman discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
Sat, 20 Aug 2011 15:54:26 -0700 huffman remove redundant lemma real_0_le_divide_iff in favor or zero_le_divide_iff
Fri, 19 Aug 2011 08:39:43 -0700 huffman fold definitions of sin_coeff and cos_coeff in Maclaurin lemmas
Fri, 19 Aug 2011 07:45:22 -0700 huffman remove some redundant simp rules
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Wed, 29 Dec 2010 17:34:41 +0100 wenzelm explicit file specifications -- avoid secondary load path;
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
less more (0) -120 tip