Sun, 16 Oct 2016 09:31:06 +0200 |
haftmann |
eliminated irregular aliasses
|
file |
diff |
annotate
|
Sun, 16 Oct 2016 09:31:05 +0200 |
haftmann |
eliminated irregular aliasses
|
file |
diff |
annotate
|
Sun, 16 Oct 2016 09:31:05 +0200 |
haftmann |
more standardized theorem names for facts involving the div and mod identity
|
file |
diff |
annotate
|
Sun, 16 Oct 2016 09:31:04 +0200 |
haftmann |
more standardized names
|
file |
diff |
annotate
|
Wed, 21 Sep 2016 17:56:25 +0200 |
immler |
approximation: preprocessing for nat/int expressions
|
file |
diff |
annotate
|
Wed, 21 Sep 2016 17:56:25 +0200 |
immler |
approximation: rewrite for reduction to base expressions
|
file |
diff |
annotate
|
Mon, 19 Sep 2016 20:06:21 +0200 |
fleury |
left_distrib ~> distrib_right, right_distrib ~> distrib_left
|
file |
diff |
annotate
|
Sun, 31 Jul 2016 18:05:20 +0200 |
wenzelm |
simplified theory structure;
|
file |
diff |
annotate
|
Sat, 09 Jul 2016 13:26:16 +0200 |
haftmann |
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
|
file |
diff |
annotate
|
Thu, 09 Jun 2016 16:04:20 +0200 |
immler |
approximation, derivative, and continuity of floor and ceiling
|
file |
diff |
annotate
|
Wed, 08 Jun 2016 16:46:48 +0200 |
immler |
generalized bitlen to floor of log
|
file |
diff |
annotate
|
Fri, 27 May 2016 20:23:55 +0200 |
wenzelm |
tuned proofs, to allow unfold_abs_def;
|
file |
diff |
annotate
|
Mon, 25 Apr 2016 16:09:26 +0200 |
wenzelm |
eliminated old 'def';
|
file |
diff |
annotate
|
Tue, 23 Feb 2016 16:25:08 +0100 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
Tue, 19 Jan 2016 07:59:29 +0100 |
Manuel Eberl |
Made Approximation work for powr again
|
file |
diff |
annotate
|
Tue, 29 Dec 2015 23:04:53 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
Mon, 28 Dec 2015 01:28:28 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
Thu, 10 Dec 2015 13:38:40 +0000 |
paulson |
not_leE -> not_le_imp_less and other tidying
|
file |
diff |
annotate
|
Fri, 13 Nov 2015 12:27:13 +0000 |
paulson |
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
|
file |
diff |
annotate
|
Tue, 10 Nov 2015 14:43:29 +0000 |
paulson |
Merge
|
file |
diff |
annotate
|
Tue, 10 Nov 2015 14:18:41 +0000 |
paulson |
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
|
file |
diff |
annotate
|
Thu, 05 Nov 2015 10:39:59 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
Tue, 07 Jul 2015 00:48:42 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
Sat, 20 Jun 2015 16:31:44 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
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.
|
file |
diff |
annotate
|
Mon, 30 Mar 2015 10:52:54 +0200 |
eberlm |
exposed approximation in ML
|
file |
diff |
annotate
|
Thu, 19 Mar 2015 14:24:51 +0000 |
paulson |
New material for complex sin, cos, tan, Ln, also some reorganisation
|
file |
diff |
annotate
|
Wed, 18 Mar 2015 14:13:27 +0000 |
paulson |
Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
|
file |
diff |
annotate
|
Mon, 16 Mar 2015 15:30:00 +0000 |
paulson |
The factorial function, "fact", now has type "nat => 'a"
|
file |
diff |
annotate
|
Mon, 09 Mar 2015 16:28:19 +0000 |
paulson |
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
|
file |
diff |
annotate
|
Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
Tue, 03 Mar 2015 19:08:04 +0100 |
traytel |
eliminated some clones of Proof_Context.cterm_of
|
file |
diff |
annotate
|
Tue, 10 Feb 2015 14:48:26 +0100 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
file |
diff |
annotate
|
Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
Wed, 12 Nov 2014 17:37:43 +0100 |
immler |
added quickcheck[approximation]
|
file |
diff |
annotate
|
Wed, 12 Nov 2014 17:37:43 +0100 |
immler |
disjunction and conjunction for forms
|
file |
diff |
annotate
|
Wed, 12 Nov 2014 17:37:43 +0100 |
immler |
truncate intermediate results in horner to improve performance of approximate;
|
file |
diff |
annotate
|
Wed, 12 Nov 2014 17:36:29 +0100 |
immler |
simplified computations based on round_up by reducing to round_down;
|
file |
diff |
annotate
|
Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
Thu, 30 Oct 2014 21:02:01 +0100 |
haftmann |
more simp rules concerning dvd and even/odd
|
file |
diff |
annotate
|
Sun, 19 Oct 2014 18:05:26 +0200 |
haftmann |
prefer generic elimination rules for even/odd over specialized unfold rules for nat
|
file |
diff |
annotate
|
Sun, 21 Sep 2014 16:56:11 +0200 |
haftmann |
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
|
file |
diff |
annotate
|
Thu, 11 Sep 2014 19:32:36 +0200 |
blanchet |
updated news
|
file |
diff |
annotate
|
Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
|
file |
diff |
annotate
|
Fri, 04 Jul 2014 20:18:47 +0200 |
haftmann |
reduced name variants for assoc and commute on plus and mult
|
file |
diff |
annotate
|
Sat, 28 Jun 2014 09:16:42 +0200 |
haftmann |
fact consolidation
|
file |
diff |
annotate
|
Fri, 09 May 2014 08:13:36 +0200 |
haftmann |
prefer separate command for approximation
|
file |
diff |
annotate
|
Wed, 07 May 2014 12:25:35 +0200 |
hoelzl |
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
|
file |
diff |
annotate
|
Thu, 01 May 2014 10:20:20 +0200 |
haftmann |
separate ML module
|
file |
diff |
annotate
|
Mon, 14 Apr 2014 13:08:17 +0200 |
hoelzl |
added divide_nonneg_nonneg and co; made it a simp rule
|
file |
diff |
annotate
|
Sat, 12 Apr 2014 17:26:27 +0200 |
nipkow |
made mult_pos_pos a simp rule
|
file |
diff |
annotate
|
Fri, 11 Apr 2014 22:53:33 +0200 |
nipkow |
made divide_pos_pos a simp rule
|
file |
diff |
annotate
|
Fri, 11 Apr 2014 13:36:57 +0200 |
nipkow |
made mult_nonneg_nonneg a simp rule
|
file |
diff |
annotate
|
Wed, 09 Apr 2014 13:15:21 +0200 |
hoelzl |
generalize ln/log_powr; add log_base_powr/pow
|
file |
diff |
annotate
|
Wed, 09 Apr 2014 09:37:47 +0200 |
hoelzl |
revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
|
file |
diff |
annotate
|
Fri, 04 Apr 2014 17:58:25 +0100 |
paulson |
divide_minus_left divide_minus_right are in field_simps but are not default simprules
|
file |
diff |
annotate
|
Thu, 03 Apr 2014 18:24:08 +0200 |
hoelzl |
fix #0556204bc230
|
file |
diff |
annotate
|
Thu, 03 Apr 2014 17:56:08 +0200 |
hoelzl |
merged DERIV_intros, has_derivative_intros into derivative_intros
|
file |
diff |
annotate
|
Tue, 18 Mar 2014 11:58:30 -0700 |
huffman |
adapt to Isabelle/c726ecfb22b6
|
file |
diff |
annotate
|
Thu, 13 Mar 2014 07:07:07 +0100 |
nipkow |
enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions
|
file |
diff |
annotate
|
Sat, 15 Feb 2014 18:48:43 +0100 |
wenzelm |
removed dead code;
|
file |
diff |
annotate
|
Fri, 14 Feb 2014 07:53:46 +0100 |
blanchet |
merged 'Option.map' and 'Option.map_option'
|
file |
diff |
annotate
|
Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
renamed '{prod,sum,bool,unit}_case' to 'case_...'
|
file |
diff |
annotate
|
Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
adapted theories to '{case,rec}_{list,option}' names
|
file |
diff |
annotate
|
Mon, 16 Dec 2013 17:08:22 +0100 |
immler |
additional definitions and lemmas for Float
|
file |
diff |
annotate
|
Tue, 19 Nov 2013 10:05:53 +0100 |
haftmann |
eliminiated neg_numeral in favour of - (numeral _)
|
file |
diff |
annotate
|
Tue, 05 Nov 2013 15:10:59 +0100 |
hoelzl |
tuned proofs in Approximation
|
file |
diff |
annotate
|
Fri, 01 Nov 2013 18:51:14 +0100 |
haftmann |
more simplification rules on unary and binary minus
|
file |
diff |
annotate
|
Sun, 18 Aug 2013 19:59:19 +0200 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
Sun, 02 Jun 2013 07:46:40 +0200 |
haftmann |
make reification part of HOL
|
file |
diff |
annotate
|
Fri, 31 May 2013 09:30:32 +0200 |
haftmann |
decomposed reflection steps into conversions;
|
file |
diff |
annotate
|
Fri, 31 May 2013 09:30:32 +0200 |
haftmann |
dropped vacuous prefix
|
file |
diff |
annotate
|
Fri, 24 May 2013 17:00:46 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Mon, 20 May 2013 20:47:33 +0200 |
wenzelm |
proper context;
|
file |
diff |
annotate
|
Sun, 21 Apr 2013 10:41:18 +0200 |
haftmann |
combined reify_data.ML into reflection.ML;
|
file |
diff |
annotate
|
Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
Tue, 26 Mar 2013 20:37:32 +0100 |
wenzelm |
tuned session specification;
|
file |
diff |
annotate
|
Fri, 15 Feb 2013 08:31:31 +0100 |
haftmann |
two target language numeral types: integer and natural, as replacement for code_numeral;
|
file |
diff |
annotate
|
Fri, 19 Oct 2012 15:12:52 +0200 |
webertj |
Renamed {left,right}_distrib to distrib_{right,left}.
|
file |
diff |
annotate
|
Thu, 13 Sep 2012 17:20:04 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
Fri, 20 Apr 2012 11:14:39 +0200 |
hoelzl |
hide code generation facts in the Float theory, they are only exported for Approximation
|
file |
diff |
annotate
|
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
|
file |
diff |
annotate
|
Wed, 18 Apr 2012 14:29:22 +0200 |
hoelzl |
use lifting to introduce floating point numbers
|
file |
diff |
annotate
|
Wed, 18 Apr 2012 14:29:21 +0200 |
hoelzl |
replace the float datatype by a type with unique representation
|
file |
diff |
annotate
|
Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
Sun, 12 Feb 2012 22:10:05 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
|
Sun, 13 Nov 2011 19:30:35 +0100 |
huffman |
remove lemma float_remove_real_numeral, which duplicated Float.float_number_of
|
file |
diff |
annotate
|
Wed, 12 Oct 2011 20:16:48 +0200 |
wenzelm |
tuned proofs -- eliminated vacuous "induct arbitrary: ..." situations;
|
file |
diff |
annotate
|
Wed, 07 Sep 2011 09:02:58 -0700 |
huffman |
avoid using legacy theorem names
|
file |
diff |
annotate
|
Sun, 28 Aug 2011 09:20:12 -0700 |
huffman |
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
|
file |
diff |
annotate
|
Sat, 20 Aug 2011 15:54:26 -0700 |
huffman |
remove redundant lemma real_0_le_divide_iff in favor or zero_le_divide_iff
|
file |
diff |
annotate
|
Fri, 19 Aug 2011 08:39:43 -0700 |
huffman |
fold definitions of sin_coeff and cos_coeff in Maclaurin lemmas
|
file |
diff |
annotate
|
Fri, 19 Aug 2011 07:45:22 -0700 |
huffman |
remove some redundant simp rules
|
file |
diff |
annotate
|
Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
Wed, 29 Dec 2010 17:34:41 +0100 |
wenzelm |
explicit file specifications -- avoid secondary load path;
|
file |
diff |
annotate
|
Mon, 06 Dec 2010 19:54:48 +0100 |
hoelzl |
move coercions to appropriate places
|
file |
diff |
annotate
|
Mon, 06 Dec 2010 19:18:02 +0100 |
nipkow |
moved coercion decl. for int
|
file |
diff |
annotate
|
Thu, 02 Dec 2010 21:23:56 +0100 |
wenzelm |
proper theory name (cf. e84f82418e09);
|
file |
diff |
annotate
|
Thu, 02 Dec 2010 16:16:18 +0100 |
hoelzl |
Use coercions in Approximation (by Dmitriy Traytel).
|
file |
diff |
annotate
|
Mon, 20 Sep 2010 15:29:53 +0200 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
Sat, 28 Aug 2010 16:14:32 +0200 |
haftmann |
formerly unnamed infix equality now named HOL.eq
|
file |
diff |
annotate
|
Thu, 26 Aug 2010 20:51:17 +0200 |
haftmann |
formerly unnamed infix impliciation now named HOL.implies
|
file |
diff |
annotate
|
Wed, 25 Aug 2010 18:38:49 +0200 |
wenzelm |
approximation_oracle: actually match true/false in ML, not arbitrary values;
|
file |
diff |
annotate
|
Thu, 19 Aug 2010 16:08:59 +0200 |
haftmann |
tuned quotes
|
file |
diff |
annotate
|
Thu, 19 Aug 2010 11:02:14 +0200 |
haftmann |
use antiquotations for remaining unqualified constants in HOL
|
file |
diff |
annotate
|
Mon, 19 Jul 2010 16:09:44 +0200 |
haftmann |
diff_minus subsumes diff_def
|
file |
diff |
annotate
|
Thu, 01 Jul 2010 16:54:42 +0200 |
haftmann |
qualified constants Set.member and Set.Collect
|
file |
diff |
annotate
|
Mon, 14 Jun 2010 15:10:36 +0200 |
haftmann |
removed simplifier congruence rule of "prod_case"
|
file |
diff |
annotate
|
Thu, 10 Jun 2010 12:24:03 +0200 |
haftmann |
tuned quotes, antiquotations and whitespace
|
file |
diff |
annotate
|
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
|
file |
diff |
annotate
|
Mon, 17 May 2010 23:54:15 +0200 |
wenzelm |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
|
file |
diff |
annotate
|
Sun, 09 May 2010 22:51:11 -0700 |
huffman |
avoid using real-specific versions of generic lemmas
|
file |
diff |
annotate
|
Thu, 29 Apr 2010 15:00:40 +0200 |
haftmann |
code_reflect: specify module name directly after keyword
|
file |
diff |
annotate
|
Wed, 28 Apr 2010 21:41:05 +0200 |
haftmann |
use code_reflect
|
file |
diff |
annotate
|
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;
|
file |
diff |
annotate
|
Tue, 23 Feb 2010 12:35:32 -0800 |
huffman |
adapt to new realpow rules
|
file |
diff |
annotate
|
Wed, 10 Feb 2010 08:49:25 +0100 |
haftmann |
rely less on ordered rewriting
|
file |
diff |
annotate
|
Fri, 05 Feb 2010 14:33:50 +0100 |
haftmann |
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
|
file |
diff |
annotate
|
Tue, 20 Oct 2009 21:22:37 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|