src/Pure/Isar/isar_cmd.ML
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 *** MESSAGE REFERS TO PREVIOUS VERSION ***
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.
2004-10-01 ago display-drafts now uses pdf!
2004-09-27 ago Modified locales: improved implementation of "includes".
2004-08-12 ago Disallowed "includes" in locale declarations.
2004-06-21 ago Merged in license change from Isabelle2004
2004-06-15 ago path instead of string;
2004-06-13 ago added display_drafts and print_drafts commands;
2003-02-03 ago Moved print_intros from proof_general.ML to Isar/isar_cmd.ML
2002-07-02 ago thms_containing: optional limit argument;
2002-07-02 ago ProofContext.print_thms_containing;
2002-02-26 ago markup commands: proper theory/proof transactions!
2002-02-25 ago markup commands (from isar_thy.ML) with proper check of antiquotations;
2002-02-12 ago got rid of explicit marginal comments (now stripped earlier from input);
2002-01-15 ago print_locale: allow full body specification;
2001-12-05 ago added print_rules;
2001-11-24 ago print_locale: expr;
2001-11-09 ago Commands prf and full_prf can now also be used to display proof term
2001-11-06 ago print_syntax: include local version;
2001-11-06 ago added print_locales, print_locale;
2001-11-05 ago pretty/print functions with context;
2001-10-04 ago added print_induct_rules;