NEWS
2016-03-22 blanchet 2016-03-22 document addition of 'corec'
2016-03-19 haftmann 2016-03-19 unified CHAR with CHR syntax
2016-03-18 wenzelm 2016-03-18 recovered from Unicode accident in 7248d106c607;
2016-03-18 wenzelm 2016-03-18 merged
2016-03-17 wenzelm 2016-03-17 @{make_string} is available during Pure bootstrap;
2016-03-18 Andreas Lochbihler 2016-03-18 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
2016-03-16 wenzelm 2016-03-16 eliminated spurious Unicode, which is in conflict with Isabelle symbol interpretation;
2016-03-16 wenzelm 2016-03-16 NEWS;
2016-03-12 haftmann 2016-03-12 spelling
2016-03-12 haftmann 2016-03-12 model characters directly as range 0..255 * * * operate on syntax terms rather than asts
2016-03-10 wenzelm 2016-03-10 tuned;
2016-03-10 wenzelm 2016-03-10 isabelle_process is superseded by "isabelle process" tool; tuned tool usage; misc updates and tuning of "system" manual;
2016-03-09 wenzelm 2016-03-09 merged
2016-03-08 wenzelm 2016-03-08 back to external line editor, due to problems of JLine with multithreading of in vs. out;
2016-03-08 wenzelm 2016-03-08 isabelle console is based on Isabelle/Scala;
2016-03-07 wenzelm 2016-03-07 discontinued cd, pwd;
2016-03-07 wenzelm 2016-03-07 File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output; clarified treatment of whitespace in some bash scripts;
2016-03-08 haftmann 2016-03-08 syntax for multiset membership modelled after syntax for set membership
2016-03-07 blanchet 2016-03-07 made 'size' plugin compatible with locales again (and added regression test)
2016-03-05 wenzelm 2016-03-05 NEWS after Isabelle2016;
2016-03-05 wenzelm 2016-03-05 abbreviations for \<nexists>;
2016-03-05 wenzelm 2016-03-05 old HOL syntax is for input only;
2016-03-05 wenzelm 2016-03-05 tuned signature -- clarified modules;
2016-03-05 wenzelm 2016-03-05 tuned signature;
2016-03-03 wenzelm 2016-03-03 isabelle console -r" helps to bootstrap Isabelle/Pure;
2016-03-03 wenzelm 2016-03-03 clarified isabelle_process;
2016-03-03 wenzelm 2016-03-03 discontinued polyml-5.3.0;
2016-03-02 wenzelm 2016-03-02 support for ML_exception_debugger;
2016-02-29 wenzelm 2016-02-29 clarified session; tuned headers;
2016-02-29 wenzelm 2016-02-29 isabelle_process executable no longer supports writable heap images;
2016-02-28 wenzelm 2016-02-28 discontinued old 'header';
2016-02-28 wenzelm 2016-02-28 removed pointless "isabelle yxml";
2016-02-27 wenzelm 2016-02-27 symbol interpretation for \<circle>;
2016-02-26 haftmann 2016-02-26 more succint formulation of membership for multisets, similar to lists; discontinued ASCII notation for multiset membership; more theorems on multisets, dropping redundant interpretation; modernized notation; some annotations concerning future work
2016-02-25 wenzelm 2016-02-25 isabelle_scala_script is usually found by PATH;
2016-02-25 paulson 2016-02-25 Conformal_mappings: a big development in complex analysis (+ some lemmas)
2016-02-25 wenzelm 2016-02-25 tuned;
2016-02-24 nipkow 2016-02-24 NEWS
2016-02-10 hoelzl 2016-02-10 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.
2016-02-18 haftmann 2016-02-18 NEWS concerning 66a381d3f88f
2016-02-17 wenzelm 2016-02-17 merged
2016-02-17 wenzelm 2016-02-17 SML/NJ is no longer supported;
2016-02-17 haftmann 2016-02-17 dropped various legacy fact bindings and tuned proofs
2016-02-17 haftmann 2016-02-17 separated potentially conflicting type class instance into separate theory
2016-02-17 haftmann 2016-02-17 dropped various legacy fact bindings
2016-02-17 haftmann 2016-02-17 generalized some lemmas; moved some lemmas in more appropriate places; deleted potentially dangerous simp rule
2016-02-17 haftmann 2016-02-17 further generalization and polishing
2016-02-17 haftmann 2016-02-17 prefer abbreviations for compound operators INFIMUM and SUPREMUM
2016-02-17 blanchet 2016-02-17 making 'pred_inject' a first-class BNF citizen
2016-02-17 traytel 2016-02-17 NEWS
2016-02-17 blanchet 2016-02-17 document new 'primrec' feature
2016-02-14 wenzelm 2016-02-14 command '\<proof>' is an alias for 'sorry', with different typesetting;
2016-02-12 wenzelm 2016-02-12 merged
2016-02-01 wenzelm 2016-02-01 tuned NEWS: long-running tasks can still prevent urgent tasks from being started, due to start_execution pri = 0;
2016-01-31 wenzelm 2016-01-31 more on "ML debugging within the Prover IDE";
2016-01-24 wenzelm 2016-01-24 proper NEWS for this release;
2016-01-24 wenzelm 2016-01-24 tuned;
2016-01-24 wenzelm 2016-01-24 discontinued irregular abbrevs: ".o" counts as word, "+o", "*o", "-o" are occasionally used as ASCII notation, "*o" is in conflict with "(*o" in comments;
2016-01-22 wenzelm 2016-01-22 tuned markup, e.g. relevant for Rendering.tooltip;
2016-01-20 wenzelm 2016-01-20 back to post-release mode -- after fork point;