NEWS
2016-05-14 ago toplevel theorem statements support 'if'/'for' eigen-context;
2016-05-10 ago Theory of polyhedra: faces, extreme points, polytopes, and the Krein–Milman
2016-04-28 ago NEWS;
2016-04-26 ago 'obtain' supports structured statements (similar to 'define');
2016-04-25 ago old 'def' is legacy;
2016-04-24 ago added Isar command 'define';
2016-04-20 ago reactivated other_id reports (see also db929027e701, 8eda56033203);
2016-04-19 ago more IDE support for Isabelle/Pure bootstrap;
2016-04-15 ago merged
2016-04-14 ago highlighting of entity def/ref positions wrt. cursor;
2016-04-14 ago change is incompatible
2016-04-14 ago Probability: move emeasure and nn_integral from ereal to ennreal
2016-04-13 ago eliminated "xname" and variants;
2016-04-12 ago tuned;
2016-04-12 ago Type_Infer.object_logic controls improvement of type inference result;
2016-04-09 ago removed old proof method "default";
2016-04-09 ago support ROOT0.ML as well -- independently of ROOT.ML;
2016-04-07 ago NEWS;
2016-04-06 ago simplified bootstrap: critical structures remain accessible in ML_Root context;
2016-04-05 ago clarified bootstrap environment;
2016-04-04 ago tuned;
2016-04-04 ago option ML_system_unsafe;
2016-04-04 ago added reference from NEWS to docs
2016-04-03 ago renamed ISABELLE_BUILD_JAVA_OPTIONS to ISABELLE_TOOL_JAVA_OPTIONS;
2016-04-01 ago documentation;
2016-04-01 ago explicit property for unbreakable block;
2016-03-22 ago document addition of 'corec'
2016-03-19 ago unified CHAR with CHR syntax
2016-03-18 ago recovered from Unicode accident in 7248d106c607;
2016-03-18 ago merged
2016-03-17 ago @{make_string} is available during Pure bootstrap;
2016-03-18 ago move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
2016-03-16 ago eliminated spurious Unicode, which is in conflict with Isabelle symbol interpretation;
2016-03-16 ago NEWS;
2016-03-12 ago spelling
2016-03-12 ago model characters directly as range 0..255
2016-03-10 ago tuned;
2016-03-10 ago isabelle_process is superseded by "isabelle process" tool;
2016-03-09 ago merged
2016-03-08 ago back to external line editor, due to problems of JLine with multithreading of in vs. out;
2016-03-08 ago isabelle console is based on Isabelle/Scala;
2016-03-07 ago discontinued cd, pwd;
2016-03-07 ago File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output;
2016-03-08 ago syntax for multiset membership modelled after syntax for set membership
2016-03-07 ago made 'size' plugin compatible with locales again (and added regression test)
2016-03-05 ago NEWS after Isabelle2016;
2016-03-05 ago abbreviations for \<nexists>;
2016-03-05 ago old HOL syntax is for input only;
2016-03-05 ago tuned signature -- clarified modules;
2016-03-05 ago tuned signature;
2016-03-03 ago isabelle console -r" helps to bootstrap Isabelle/Pure;
2016-03-03 ago clarified isabelle_process;
2016-03-03 ago discontinued polyml-5.3.0;
2016-03-02 ago support for ML_exception_debugger;
2016-02-29 ago clarified session;
2016-02-29 ago isabelle_process executable no longer supports writable heap images;
2016-02-28 ago discontinued old 'header';
2016-02-28 ago removed pointless "isabelle yxml";
2016-02-27 ago symbol interpretation for \<circle>;
2016-02-26 ago more succint formulation of membership for multisets, similar to lists;