2014-11-02 ago clarified legacy command;
2014-11-02 ago uniform heading commands work in any context, even in theory header;
2014-09-07 ago separated class_deps command into separate file
2014-08-19 ago tuned signature -- moved type src to Token, without aliases;
2014-08-14 ago tuned signature -- prefer self-contained user-space tool;
2014-07-25 ago old 'defs' is legacy --- slightly odd side-entry that bypasses regular Local_Theory.define interface;
2014-07-22 ago tuned messages;
2014-05-05 ago clarified print operations for "terms" and "theorems";
2014-03-31 ago some shortcuts for chunks, which sometimes avoid bulky string output;
2014-03-27 ago redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
2014-03-25 ago separate tokenization and language context for SML: no symbols, no antiquotes;
2014-03-25 ago added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
2014-03-18 ago more antiquotations;
2014-03-15 ago more explicit treatment of verbose mode, which includes concealed entries;
2014-03-15 ago clarified print_local_facts;
2014-03-12 ago tuned signature -- clarified module name;
2014-03-09 ago more formal read_root;
2014-03-09 ago simplified / modernized hide commands: proper outer parsers and PIDE markup via check;
2014-03-01 ago clarified language markup: added "delimited" property;
2013-08-23 ago added Theory.setup convenience;
2013-07-07 ago discontinued command 'print_drafts';
2013-05-25 ago syntax translations always depend on context;
2013-04-18 ago simplifier uses proper Proof.context instead of historic type simpset;
2013-03-30 ago item markup for Proof_Context.pretty_fact;
2013-01-05 ago tuned -- less indirection;
2012-10-17 ago more method position information, notably finished_pos after end of previous text;
2012-10-16 ago more proof method text position information;
2012-09-26 ago tuned pretty_locale/print_locale, with more basic pretty_locale_deps based on that;
2012-09-25 ago separate module Graph_Display;
2012-08-30 ago refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
2012-08-24 ago check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
2012-08-22 ago clarified Parse.path vs. Parse.explode -- prefer errors in proper transaction context;
2012-08-14 ago support for 'typ' with explicit sort constraint;
2012-08-11 ago faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
2012-04-27 ago clarified signature;
2012-03-14 ago source positions for locale and class expressions;
2011-11-28 ago separate module for concrete Isabelle markup;
2011-11-14 ago pass positions for named targets, for formal links in the document model;
2011-10-28 ago uniform Local_Theory.declaration with explicit params;
2011-08-20 ago refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
2011-06-27 ago document antiquotations are managed as theory data, with proper name space and entity markup;
2011-06-27 ago ML antiquotations are managed as theory data, with proper name space and entity markup;
2011-04-23 ago proper binding/report of defined simprocs;
2011-04-20 ago added Theory.nodes_of convenience;
2011-04-16 ago modernized structure Proof_Context;
2011-04-16 ago prefer local name spaces;
2011-04-16 ago Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
2011-04-06 ago typed_print_translation: discontinued show_sorts argument;
2011-04-06 ago renamed Standard_Syntax to Syntax_Phases;
2011-04-05 ago moved decode/parse operations to standard_syntax.ML;
2011-04-05 ago discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
2011-04-03 ago added Position.reports convenience;
2011-01-06 ago Diagnostic command to show locale dependencies.
2010-11-28 ago added 'syntax_declaration' command;
2010-11-27 ago more explicit Isabelle_System operations;
2010-11-06 ago mark 'cd' and 'commit' as control command -- not usable in asynchronous document model, likely to cause confusion in Proof General;
2010-09-20 ago renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-09-17 ago tuned signature of (Context_) variants;
2010-09-06 ago discontinued obsolete ProofContext.prems_limit;
2010-09-03 ago pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;