2007-06-26 ago fixed undo: try undos_proof first!
2007-05-08 ago tuned ProofDisplay.pretty_full_theory;
2007-04-05 ago thy_deps: sort Context.thy_ord;
2007-04-04 ago simplified thy_deps using Theory.ancestors_of (in order of creation);
2007-04-03 ago avoid clash with Alice keywords;
2007-03-20 ago added theory dependency graph
2007-02-20 ago Remove duplicates from printed theorems in find_theorems
2007-02-04 ago tuned oracle interface;
2007-01-28 ago added simproc_setup;
2007-01-19 ago added various ML setup functions (from sign.ML, pure_thy.ML);
2007-01-19 ago added 'declaration' command;
2006-12-30 ago removed obsolete clear_undos_theory;
2006-12-29 ago removed obsolete init_context;
2006-12-15 ago avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
2006-12-09 ago added print_abbrevs;
2006-12-05 ago print_syntax etc.: plain Toplevel.context_of;
2006-11-28 ago dest_term: strip_imp_concl;
2006-11-23 ago prefer Proof.context over Context.generic;
2006-11-21 ago moved theorem kinds from PureThy to Thm;
2006-11-14 ago incorporated IsarThy into IsarCmd;
2006-10-12 ago renamed print_lthms to print_facts, do not insist on proof state;
2006-10-11 ago removed 'undo_end', recovered 'cannot_undo';
2006-10-11 ago undo_end/kill: handle local theory;
2006-10-09 ago Secure.commit;
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-04-13 ago ProofDisplay.print_theorems/theory;
2006-04-09 ago print_term etc.: actually observe print mode in final output;
2006-03-14 ago added print_stmts;
2006-02-15 ago simplified presentation commands;
2006-01-27 ago Locale.init;
2006-01-10 ago print rules: generic context;
2006-01-05 ago tuned print_theorems_theory;
2005-11-09 ago Element.context;
2005-11-02 ago Isar.loop;
2005-10-18 ago back: Toplevel.actual/skip_proof;
2005-09-13 ago Proof.get_thmss;
2005-09-05 ago add_chapter/section/subsection/subsubsection/text: optional locale specification;
2005-09-02 ago print_locale omits facts by default
2005-08-31 ago present_text: Toplevel.no_body_context prevents use of wrong context in interaction;
2005-08-24 ago Printing of interpretations: option to show witness theorems;
2005-08-16 ago back: removed ill-defined '!' option;
2005-07-13 ago Toplevel.actual_proof;
2005-06-20 ago print_theorems: proper use of PureThy.print_theorems_diff;
2005-06-05 ago File.shell_path;
2005-06-02 ago tuned comment;
2005-05-23 ago use: not a theory command!
2005-05-22 ago string FindTheorems.criterion;
2005-05-22 ago added print_simpset;
2005-05-17 ago tuned;
2005-05-16 ago searching for thms by combination of criteria (intro, elim, dest, name, term pattern)
2005-04-21 ago Adapted use command to new behaviour of Toplevel.node_trans
2005-04-13 ago *** empty log message ***
2005-03-24 ago Further work on interpretation commands. New command `interpret' for
2005-03-09 ago First version of global registration command.
2005-02-13 ago Deleted Library.option type.
2005-01-24 ago Specific theorems in a named list of theorems can now be referred to
2004-10-11 ago Some changes to allow skipping of proof scripts.