2001-12-05 ago added 'print_rules' command;
2001-11-24 ago print_locale: expr;
2001-11-22 ago import locale expression;
2001-11-22 ago tuned;
2001-11-19 ago improved treatment of common result name;
2001-11-19 ago multi_theorem: common statement header (covers *all* results);
2001-11-11 ago "theorem" etc.: multiple statements;
2001-11-09 ago Commands prf and full_prf can now also be used to display proof term
2001-11-06 ago separate "in" locale vs. ad-hoc context;
2001-11-06 ago added 'locale', 'print_locales', 'print_locale';
2001-11-04 ago locale syntax;
2001-10-31 ago global statements: locale argument;
2001-10-22 ago improved source arrangement of obtain;
2001-10-16 ago support impromptu terminology of cases parameters;
2001-10-13 ago generic theorem kinds;
2001-10-04 ago added print_induct_rules;
2001-10-02 ago support non-oriented infix;
2001-08-31 ago Added functions for printing primitive proof terms.
2001-02-12 ago support \<subseteq> syntax in classes/classrel/axclass/instance;
2001-02-01 ago thms_containing: term args;
2001-01-18 ago show/thus: Toplevel.proof';
2000-12-16 ago 'def': \<equiv>;
2000-12-11 ago "translations": allow harpoons;
2000-12-04 ago dignostic commands: comment;
2000-11-13 ago tuned statement args;
2000-09-15 ago ML_command: no_timing;
2000-09-01 ago 'declare' made proper command;
2000-08-29 ago pr: added prems limit;
2000-08-14 ago added "declare" command;
2000-08-08 ago prf_heading kind;
2000-07-30 ago def: no constraint on var;
2000-07-27 ago added thm_deps;
2000-07-13 ago defs: (overloaded) option;
2000-07-06 ago allow comment in more commands;
2000-07-01 ago removed "help";
2000-06-29 ago added method_setup;
2000-06-25 ago use ThyHeader.args;
2000-06-08 ago prf_open/close;
2000-06-04 ago opt_mixfix', opt_infix';
2000-06-03 ago block commands: marginal comment;
2000-05-31 ago Toplevel.no_timing;
2000-05-24 ago added "done" proof;
2000-05-21 ago replaced {{ }} by { };
2000-05-18 ago print_state: flag for proof only;
2000-05-05 ago GPLed;
2000-04-17 ago added 'hide';
2000-04-07 ago apply etc.: comments;
2000-04-06 ago 'welcome' made diagnostic;
2000-04-05 ago removed "as" keyword;
2000-04-03 ago markup_env_command 'text' / 'txt';
2000-04-01 ago 'cd': diag;
2000-03-30 ago let_bind(_i): polymorphic version;
2000-03-26 ago added 'ultimately';
2000-03-23 ago added 'moreover' command;
2000-03-18 ago 'oops' made proper;
2000-03-17 ago generic "kill" command;
2000-03-15 ago 'pr': modes, optional limit;
2000-03-14 ago 'undo' prints state (again);
2000-03-14 ago invoke_case: include attributes;
2000-03-08 ago added 'case' command;