2011-04-17 ago report Name_Space.declare/define, relatively to context;
2011-04-16 ago prefer local name spaces;
2011-04-09 ago some position reports for 'translations';
2011-04-08 ago notation: proper markup for type constructor / constant;
2011-04-08 ago tuned signature;
2011-04-03 ago added Position.reports convenience;
2011-03-13 ago Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
2011-01-16 ago added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;
2011-01-13 ago Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;
2011-01-06 ago Diagnostic command to show locale dependencies.
2010-12-18 ago Add mixins to sublocale command.
2010-12-17 ago Command 'type_synonym' (with single argument) supersedes 'types' (legacy feature);
2010-12-17 ago replaced command 'nonterminals' by slightly modernized version 'nonterminal';
2010-12-05 ago command 'notepad' replaces former 'example_proof';
2010-12-04 ago formal notepad without any result;
2010-11-28 ago added 'syntax_declaration' command;
2010-11-07 ago 'example_proof' is treated as non-schematic statement with irrelevant proof (NB: even regular proofs can contain unreachable parts wrt. the graph of proof promises);
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-08 ago removed ancient constdefs command
2010-09-06 ago discontinued obsolete ProofContext.prems_limit;
2010-08-31 ago moved Toplevel.run_command to Pure/PIDE/document.ML;
2010-08-30 ago tuned;
2010-08-25 ago discontinued obsolete 'global' and 'local' commands;
2010-08-11 ago more convenient split of class modules: class and class_declaration
2010-08-11 ago renamed Theory_Target to the more appropriate Named_Target
2010-08-11 ago moved instantiation target formally to class_target.ML
2010-08-11 ago moved overloading target formally to overloading.ML
2010-07-31 ago Interpretation in proofs supports mixins.
2010-07-28 ago explicit Keyword.control markup for various control commands -- to prevent them from occurring in proof documents;
2010-07-27 ago theory loader: removed obsolete touch/outdate operations (require_thy no longer changes the database implicitly);
2010-07-27 ago simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
2010-07-24 ago moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
2010-07-21 ago eliminated old time_use/time_use_thy variants -- timing is implicitly controlled via Output.timing;
2010-07-20 ago warning in proper transaction context;
2010-05-31 ago modernized some structure names, keeping a few legacy aliases;
2010-05-30 ago replaced ML_Lex.read_antiq by more concise, which includes full read/report with explicit position information;
2010-05-15 ago renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
2010-05-15 ago renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
2010-05-15 ago renamed structure ValueParse to Parse_Value;
2010-05-15 ago refer directly to structure Keyword and Parse;
2010-05-12 ago updated/unified some legacy warnings;
2010-04-29 ago ProofContext.read_const: allow for type constraint (for fixed variable);
2010-04-28 ago renamed command 'defaultsort' to 'default_sort';
2010-04-28 ago localized default sort;
2010-04-28 ago modernized/simplified Sign.set_defsort;
2010-04-26 ago command 'example_proof' opens an empty proof body;
2010-04-25 ago modernized naming conventions of main Isar proof elements;
2010-04-23 ago explicit 'schematic_theorem' etc. for schematic theorem statements;
2010-04-16 ago keep localized 'types' as regular non-old-style version -- 'type_abbrev' as 'type' just causes too many problems, e.g. clash with "type" in translations or "type:" argument syntax;
2010-04-16 ago replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-04-16 ago modernized old-style type abbreviations;
2010-04-16 ago local type abbreviations;
2010-04-11 ago user interface for abstract datatypes is an attribute, not a command
2010-03-21 ago minor renovation of old-style 'axioms' -- make it an alias of iterated 'axiomatization';
2010-03-18 ago typedecl: no sort constraints;
2010-03-09 ago localized typedecl;
2010-03-07 ago separate structure Typedecl;
2010-03-07 ago modernized structure Object_Logic;
2010-03-01 ago added type_notation command;
2010-02-24 ago allow general mixfix syntax for type constructors;