| 2016-03-02 |
wenzelm |
support for ML_exception_debugger;
|
file |
diff |
annotate
|
| 2016-02-29 |
wenzelm |
clarified session;
|
file |
diff |
annotate
|
| 2016-02-29 |
wenzelm |
isabelle_process executable no longer supports writable heap images;
|
file |
diff |
annotate
|
| 2016-02-28 |
wenzelm |
discontinued old 'header';
|
file |
diff |
annotate
|
| 2016-02-28 |
wenzelm |
removed pointless "isabelle yxml";
|
file |
diff |
annotate
|
| 2016-02-27 |
wenzelm |
symbol interpretation for \<circle>;
|
file |
diff |
annotate
|
| 2016-02-26 |
haftmann |
more succint formulation of membership for multisets, similar to lists;
|
file |
diff |
annotate
|
| 2016-02-25 |
wenzelm |
isabelle_scala_script is usually found by PATH;
|
file |
diff |
annotate
|
| 2016-02-25 |
paulson |
Conformal_mappings: a big development in complex analysis (+ some lemmas)
|
file |
diff |
annotate
|
| 2016-02-24 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2016-02-24 |
nipkow |
NEWS
|
file |
diff |
annotate
|
| 2016-02-10 |
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
|
| 2016-02-18 |
haftmann |
NEWS concerning 66a381d3f88f
|
file |
diff |
annotate
|
| 2016-02-17 |
wenzelm |
merged
|
file |
diff |
annotate
|
| 2016-02-17 |
wenzelm |
SML/NJ is no longer supported;
|
file |
diff |
annotate
|
| 2016-02-17 |
haftmann |
dropped various legacy fact bindings and tuned proofs
|
file |
diff |
annotate
|
| 2016-02-17 |
haftmann |
separated potentially conflicting type class instance into separate theory
|
file |
diff |
annotate
|
| 2016-02-17 |
haftmann |
dropped various legacy fact bindings
|
file |
diff |
annotate
|
| 2016-02-17 |
haftmann |
generalized some lemmas;
|
file |
diff |
annotate
|
| 2016-02-17 |
haftmann |
further generalization and polishing
|
file |
diff |
annotate
|
| 2016-02-17 |
haftmann |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
file |
diff |
annotate
|
| 2016-02-17 |
blanchet |
making 'pred_inject' a first-class BNF citizen
|
file |
diff |
annotate
|
| 2016-02-17 |
traytel |
NEWS
|
file |
diff |
annotate
|
| 2016-02-17 |
blanchet |
document new 'primrec' feature
|
file |
diff |
annotate
|
| 2016-02-14 |
wenzelm |
command '\<proof>' is an alias for 'sorry', with different typesetting;
|
file |
diff |
annotate
|
| 2016-02-12 |
wenzelm |
merged
|
file |
diff |
annotate
|
| 2016-02-01 |
wenzelm |
tuned NEWS: long-running tasks can still prevent urgent tasks from being started, due to start_execution pri = 0;
|
file |
diff |
annotate
|
| 2016-01-31 |
wenzelm |
more on "ML debugging within the Prover IDE";
|
file |
diff |
annotate
|
| 2016-01-24 |
wenzelm |
proper NEWS for this release;
|
file |
diff |
annotate
|
| 2016-01-24 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2016-01-24 |
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
|
| 2016-01-22 |
wenzelm |
tuned markup, e.g. relevant for Rendering.tooltip;
|
file |
diff |
annotate
|
| 2016-01-20 |
wenzelm |
back to post-release mode -- after fork point;
|
file |
diff |
annotate
|
| 2016-01-20 |
blanchet |
fixed NEWS w.r.t. multisets
|
file |
diff |
annotate
|
| 2016-01-20 |
blanchet |
added 'supset' variants for new '<#' etc. symbols on multisets
|
file |
diff |
annotate
|
| 2016-01-19 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2016-01-19 |
Manuel Eberl |
Added approximation of powr to NEWS/CONTRIBUTORS
|
file |
diff |
annotate
|
| 2016-01-13 |
wenzelm |
removed old 'defs' command;
|
file |
diff |
annotate
|
| 2016-01-13 |
wenzelm |
Eisbach works for other object-logics, e.g. Eisbach_FOL.thy;
|
file |
diff |
annotate
|
| 2016-01-13 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2016-01-13 |
blanchet |
updated NEWS
|
file |
diff |
annotate
|
| 2016-01-12 |
wenzelm |
more good NEWS;
|
file |
diff |
annotate
|
| 2016-01-11 |
kleing |
print_record NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| 2016-01-09 |
wenzelm |
generate HTML version of NEWS, with proper symbol rendering;
|
file |
diff |
annotate
|
| 2016-01-09 |
wenzelm |
merged
|
file |
diff |
annotate
|
| 2016-01-09 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2016-01-09 |
wenzelm |
\<struct> loses its rendering and is superseded by \<diamondop>;
|
file |
diff |
annotate
|
| 2016-01-09 |
wenzelm |
discontinued \<struct> syntax;
|
file |
diff |
annotate
|
| 2016-01-08 |
hoelzl |
add uniform spaces
|
file |
diff |
annotate
|
| 2016-01-08 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2016-01-08 |
wenzelm |
merged
|
file |
diff |
annotate
|
| 2016-01-07 |
wenzelm |
more uniform treatment of package internals;
|
file |
diff |
annotate
|
| 2016-01-07 |
Manuel Eberl |
Added formal power series updates to NEWS/CONTRIBUTORS
|
file |
diff |
annotate
|
| 2016-01-06 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| 2016-01-06 |
hoelzl |
add the proof of the central limit theorem
|
file |
diff |
annotate
|
| 2016-01-06 |
blanchet |
updated NEWS
|
file |
diff |
annotate
|
| 2016-01-05 |
wenzelm |
added ML antiquotation @{method};
|
file |
diff |
annotate
|
| 2016-01-05 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| 2016-01-05 |
eberlm |
Added summability/Gamma/etc. to NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| 2016-01-02 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|