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;
2006-04-30 ago AxClass.define_class;
2006-04-27 ago tuned basic list operators (flat, maps, map_filter);
2006-04-13 ago axclass: old-style concrete syntax for canonical specification format;
2006-04-11 ago 'axclass': no parameters;
2006-04-08 ago 'abbreviation': optional print mode;
2006-03-20 ago Tuned signature of Locale.add_locale(_i).
2006-03-17 ago add_locale(_i) returns internal locale name.
2006-03-14 ago added 'print_statement' command;
2006-03-14 ago added 'no_translations';
2006-03-11 ago *** empty log message ***
2006-03-08 ago constdecl: always allow 'where';
2006-02-16 ago added 'abbreviation';
2006-02-06 ago Toplevel.local_theory;
2006-02-03 ago refined signature of locale module
2006-02-02 ago moved (general_)statement to outer_parse.ML;
2006-01-28 ago removed obsolete keyword 'files';
2006-01-27 ago moved theorem tags from Drule to PureThy;
2006-01-25 ago added 'definition';
2006-01-24 ago axiomatization: optional vars;
2006-01-13 ago uniform handling of fixes;
2006-01-07 ago added 'axiomatization';
2006-01-04 ago Toplevel.forget_proof;
2006-01-03 ago added 'using' command;
2005-11-30 ago simulaneous 'def';
2005-11-10 ago guess: Toplevel.proof;
2005-11-09 ago P.context_element, P.locale_element;
2005-10-18 ago use simplified Toplevel.proof etc.;
2005-10-15 ago added 'guess';