2008-06-25 ago moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
2008-06-14 ago removed exotic 'token_translation' command;
2008-06-10 ago dropped instance with attached definitions
2008-05-24 ago more uniform treatment of OuterSyntax.local_theory commands;
2008-05-14 ago remobed obsolete keyword concl;
2008-04-15 ago proof endings: no Toplevel.print!
2008-04-15 ago IsarCmd.hide_names;
2008-04-10 ago eliminated unused Toplevel.print3/three_buffers;
2008-04-02 ago removed obscure "attach" feature
2008-03-29 ago commands 'use' and 'ML' now thy_decl;
2008-03-27 ago eliminated delayed theory setup
2008-03-26 ago use_thy: removed obsolete;
2008-03-25 ago added 'ML_val' command (diagnostic);
2008-03-24 ago ML runtime compilation: pass position, tuned signature;
2008-03-10 ago dropped "include" feature of classes
2008-02-28 ago Added unused_thms command.
2008-02-09 ago overloading: tuned signature;
2008-01-08 ago refined overloading target
2008-01-02 ago Isabelle.command: IsarCmd.nested_command (with properties);
2007-12-14 ago nested commands: avoid nested errors;
2007-12-08 ago tuned message;
2007-12-08 ago tuned messages;
2007-12-07 ago added nested 'Isabelle.command';
2007-12-05 ago improved
2007-12-03 ago overloading target
2007-11-29 ago instance command as rudimentary class target
2007-11-28 ago ObjectLogic.typedecl;
2007-11-28 ago tuned interfaces of class module
2007-11-23 ago rudimentary instantiation target
2007-11-05 ago TheoryTarget.context;
2007-11-02 ago clarified theory target interface
2007-10-25 ago made command 'undo' silent ('ProofGeneral.undo' becomes a historical relic);
2007-10-19 ago sorry: proper command;
2007-10-12 ago dropped local_syntax
2007-10-11 ago renamed Syntax.XXX_mode to Syntax.mode_XXX;
2007-10-11 ago 'notation': allow 'structure' as well;
2007-10-10 ago added 'no_notation';
2007-10-09 ago class: print result is for locale;
2007-10-09 ago AxClass.axiomatize and Specification: renamed XXX_i to XXX, and XXX to XXX_cmd;
2007-10-08 ago added proper subclass concept; improved class target
2007-10-06 ago tuned;
2007-10-06 ago simplified interfaces for outer syntax;
2007-10-04 ago moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
2007-09-29 ago proper syntax during class specification
2007-09-18 ago distinction between regular and default code theorems
2007-09-15 ago clarified class interfaces and internals
2007-08-28 ago Specification.theorem now also takes "interactive" flag as argument.
2007-08-24 ago overloaded definitions accompanied by explicit constants
2007-08-17 ago removed obsolete touch_all_thys;
2007-08-10 ago new structure for code generator modules
2007-08-07 ago theory loader: removed obsolete update_thy (coincides with use_thy);
2007-08-01 ago renamed 'print_options' to 'print_configs';
2007-07-25 ago added command 'print_options';
2007-07-19 ago removed obsolete use/update_thy_only;
2007-07-12 ago command 'declare': proper thy_decl;
2007-05-08 ago tuned;
2007-04-26 ago renamed some old names to;
2007-04-20 ago Isar definitions are now added explicitly to code theorem table
2007-04-03 ago avoid clash with Alice keywords;
2007-03-20 ago added theory dependency graph