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
2007-03-06 ago fix wrong default for find_theorems
2007-03-06 ago find_theorems: moved with_dup into the brackets, i.e.
2007-03-02 ago syntax for "class attach const"
2007-02-23 ago locale: add_locale accepts explicit predicate name, interpretation supports non-mandatory prefixes
2007-02-20 ago Remove duplicates from printed theorems in find_theorems
2007-02-16 ago unified arity parser/arguments;
2007-02-14 ago class package now using Locale.interpretation_i
2007-02-10 ago moved commands of class package here
2007-02-04 ago tuned oracle interface;
2007-01-28 ago added simproc_setup;
2007-01-19 ago renamed IsarOutput to ThyOutput;
2007-01-19 ago added 'declaration' command;
2006-12-30 ago removed obsolete 'clear_undos';
2006-12-29 ago changed syntax for axclass attach
2006-12-14 ago locale: print context for begin;
2006-12-12 ago classified show/thus as prf_asm_goal, which is usually hilited in PG;
2006-12-09 ago added 'print_abbrevs';
2006-12-08 ago added 'help' command (same of 'print_commands');
2006-12-07 ago definition/abbreviation: single argument;
2006-11-30 ago simplified syntax for 'definition', 'abbreviation';
2006-11-26 ago abbrevs: no result;
2006-11-22 ago added Isar syntax for adding parameters to axclasses
2006-11-21 ago moved theorem kinds from PureThy to Thm;
2006-11-17 ago 'notation': more robust 'and' list;
2006-11-14 ago incorporated IsarThy into IsarCmd;
2006-11-11 ago turned 'context' into plain thy_decl, discontinued thy_switch;
2006-11-09 ago abbrevs: return result;
2006-11-07 ago removed obsolete Locale.smart_theorem;