| Wed, 10 Feb 2016 18:43:19 +0100 |
hoelzl |
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
|
file |
diff |
annotate
|
| Thu, 18 Feb 2016 17:07:10 +0100 |
haftmann |
NEWS concerning 66a381d3f88f
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 23:29:35 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 23:06:24 +0100 |
wenzelm |
SML/NJ is no longer supported;
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:58 +0100 |
haftmann |
dropped various legacy fact bindings and tuned proofs
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:58 +0100 |
haftmann |
separated potentially conflicting type class instance into separate theory
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:57 +0100 |
haftmann |
dropped various legacy fact bindings
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:57 +0100 |
haftmann |
generalized some lemmas;
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:56 +0100 |
haftmann |
further generalization and polishing
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:56 +0100 |
haftmann |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 17:08:36 +0100 |
blanchet |
making 'pred_inject' a first-class BNF citizen
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 15:41:28 +0100 |
traytel |
NEWS
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 12:07:49 +0100 |
blanchet |
document new 'primrec' feature
|
file |
diff |
annotate
|
| Sun, 14 Feb 2016 16:30:27 +0100 |
wenzelm |
command '\<proof>' is an alias for 'sorry', with different typesetting;
|
file |
diff |
annotate
|
| Fri, 12 Feb 2016 22:36:48 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Mon, 01 Feb 2016 14:10:07 +0100 |
wenzelm |
tuned NEWS: long-running tasks can still prevent urgent tasks from being started, due to start_execution pri = 0;
|
file |
diff |
annotate
|
| Sun, 31 Jan 2016 19:54:40 +0100 |
wenzelm |
more on "ML debugging within the Prover IDE";
|
file |
diff |
annotate
|
| Sun, 24 Jan 2016 13:07:50 +0100 |
wenzelm |
proper NEWS for this release;
|
file |
diff |
annotate
|
| Sun, 24 Jan 2016 12:33:09 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 24 Jan 2016 12:21:57 +0100 |
wenzelm |
discontinued irregular abbrevs: ".o" counts as word, "+o", "*o", "-o" are occasionally used as ASCII notation, "*o" is in conflict with "(*o" in comments;
|
file |
diff |
annotate
|
| Fri, 22 Jan 2016 14:46:02 +0100 |
wenzelm |
tuned markup, e.g. relevant for Rendering.tooltip;
|
file |
diff |
annotate
|
| Wed, 20 Jan 2016 20:19:05 +0100 |
wenzelm |
back to post-release mode -- after fork point;
|
file |
diff |
annotate
|
| Wed, 20 Jan 2016 18:04:41 +0100 |
blanchet |
fixed NEWS w.r.t. multisets
|
file |
diff |
annotate
|
| Wed, 20 Jan 2016 17:14:53 +0100 |
blanchet |
added 'supset' variants for new '<#' etc. symbols on multisets
|
file |
diff |
annotate
|
| Tue, 19 Jan 2016 14:00:47 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 19 Jan 2016 11:19:25 +0100 |
Manuel Eberl |
Added approximation of powr to NEWS/CONTRIBUTORS
|
file |
diff |
annotate
|
| Wed, 13 Jan 2016 16:55:56 +0100 |
wenzelm |
removed old 'defs' command;
|
file |
diff |
annotate
|
| Wed, 13 Jan 2016 16:41:32 +0100 |
wenzelm |
Eisbach works for other object-logics, e.g. Eisbach_FOL.thy;
|
file |
diff |
annotate
|
| Wed, 13 Jan 2016 15:17:11 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 13 Jan 2016 09:09:38 +0100 |
blanchet |
updated NEWS
|
file |
diff |
annotate
|
| Wed, 13 Jan 2016 00:12:43 +0100 |
wenzelm |
more good NEWS;
|
file |
diff |
annotate
|
| Sun, 10 Jan 2016 19:46:31 -0800 |
kleing |
print_record NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| Sat, 09 Jan 2016 22:22:17 +0100 |
wenzelm |
generate HTML version of NEWS, with proper symbol rendering;
|
file |
diff |
annotate
|
| Sat, 09 Jan 2016 13:31:31 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Sat, 09 Jan 2016 13:00:04 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 09 Jan 2016 12:58:57 +0100 |
wenzelm |
\<struct> loses its rendering and is superseded by \<diamondop>;
|
file |
diff |
annotate
|
| Sat, 09 Jan 2016 12:35:07 +0100 |
wenzelm |
discontinued \<struct> syntax;
|
file |
diff |
annotate
|
| Fri, 08 Jan 2016 17:40:59 +0100 |
hoelzl |
add uniform spaces
|
file |
diff |
annotate
|
| Fri, 08 Jan 2016 15:54:43 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 08 Jan 2016 15:49:01 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Thu, 07 Jan 2016 15:53:39 +0100 |
wenzelm |
more uniform treatment of package internals;
|
file |
diff |
annotate
|
| Thu, 07 Jan 2016 14:44:51 +0100 |
Manuel Eberl |
Added formal power series updates to NEWS/CONTRIBUTORS
|
file |
diff |
annotate
|
| Wed, 06 Jan 2016 16:17:50 +0100 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| Wed, 06 Jan 2016 12:18:53 +0100 |
hoelzl |
add the proof of the central limit theorem
|
file |
diff |
annotate
|
| Wed, 06 Jan 2016 13:04:31 +0100 |
blanchet |
updated NEWS
|
file |
diff |
annotate
|
| Wed, 06 Jan 2016 00:04:15 +0100 |
wenzelm |
added ML antiquotation @{method};
|
file |
diff |
annotate
|
| Tue, 05 Jan 2016 15:53:17 +0100 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| Tue, 05 Jan 2016 15:38:37 +0100 |
eberlm |
Added summability/Gamma/etc. to NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| Sat, 02 Jan 2016 13:22:46 +0100 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Fri, 01 Jan 2016 19:42:48 +0100 |
wenzelm |
oops;
|
file |
diff |
annotate
|
| Fri, 01 Jan 2016 16:39:10 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 01 Jan 2016 14:44:52 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Thu, 31 Dec 2015 21:24:58 +0100 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| Thu, 31 Dec 2015 21:06:09 +0100 |
wenzelm |
misc updates for release;
|
file |
diff |
annotate
|
| Thu, 31 Dec 2015 20:40:28 +0100 |
wenzelm |
documentation for "isabelle jedit_client";
|
file |
diff |
annotate
|
| Wed, 30 Dec 2015 18:03:23 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Wed, 30 Dec 2015 14:05:51 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Wed, 30 Dec 2015 11:21:54 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Tue, 29 Dec 2015 23:40:04 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Tue, 29 Dec 2015 23:20:11 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|