| 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
|