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;
2006-11-07 ago renamed 'const_syntax' to 'notation';
2006-10-14 ago theorem: added local_theory version;
2006-10-12 ago tuned;
2006-10-11 ago 'context': demand 'begin', support local theory;
2006-10-11 ago 'end': handle local theory;
2006-10-09 ago lemmas/theorems/declare: Specification.theorems;
2006-09-30 ago added undo_end;
2006-09-19 ago 'print_theory': bang option for full verbosity;
2006-09-18 ago added class_deps;
2006-08-09 ago locale interpretation command: after_qed;
2006-08-02 ago simplified Proof.end_block;
2006-06-11 ago fixes: include mixfix syntax;
2006-06-07 ago added 'if' and 'for' keywords;
2006-05-16 ago added 'const_syntax';
2006-05-13 ago 'defs': unchecked flag;