src/Pure/Isar/isar_cmd.ML
2006-11-28 wenzelm 2006-11-28 dest_term: strip_imp_concl;
2006-11-23 wenzelm 2006-11-23 prefer Proof.context over Context.generic;
2006-11-21 wenzelm 2006-11-21 moved theorem kinds from PureThy to Thm;
2006-11-14 wenzelm 2006-11-14 incorporated IsarThy into IsarCmd;
2006-10-12 wenzelm 2006-10-12 renamed print_lthms to print_facts, do not insist on proof state; renamed Toplevel.enter_forward_proof to Toplevel.enter_proof_body;
2006-10-11 wenzelm 2006-10-11 removed 'undo_end', recovered 'cannot_undo';
2006-10-11 wenzelm 2006-10-11 undo_end/kill: handle local theory; Toplevel: generic_theory;
2006-10-09 wenzelm 2006-10-09 Secure.commit;
2006-09-30 wenzelm 2006-09-30 added undo_end;
2006-09-19 wenzelm 2006-09-19 'print_theory': bang option for full verbosity;
2006-09-18 wenzelm 2006-09-18 added class_deps;
2006-04-13 wenzelm 2006-04-13 ProofDisplay.print_theorems/theory;
2006-04-09 wenzelm 2006-04-09 print_term etc.: actually observe print mode in final output;
2006-03-14 wenzelm 2006-03-14 added print_stmts;
2006-02-15 wenzelm 2006-02-15 simplified presentation commands;
2006-01-27 wenzelm 2006-01-27 Locale.init;
2006-01-10 wenzelm 2006-01-10 print rules: generic context;
2006-01-05 wenzelm 2006-01-05 tuned print_theorems_theory;
2005-11-09 wenzelm 2005-11-09 Element.context;
2005-11-02 wenzelm 2005-11-02 Isar.loop;
2005-10-18 wenzelm 2005-10-18 back: Toplevel.actual/skip_proof; use simplified Toplevel.proof etc.;
2005-09-13 wenzelm 2005-09-13 Proof.get_thmss;
2005-09-05 wenzelm 2005-09-05 add_chapter/section/subsection/subsubsection/text: optional locale specification;
2005-09-02 ballarin 2005-09-02 print_locale omits facts by default
2005-08-31 wenzelm 2005-08-31 present_text: Toplevel.no_body_context prevents use of wrong context in interaction;
2005-08-24 ballarin 2005-08-24 Printing of interpretations: option to show witness theorems;
2005-08-16 wenzelm 2005-08-16 back: removed ill-defined '!' option; print_theorems: print facts in proof mode; print_prfs: proper context version -- ProofContext.pretty_proof_of;
2005-07-13 wenzelm 2005-07-13 Toplevel.actual_proof;
2005-06-20 wenzelm 2005-06-20 print_theorems: proper use of PureThy.print_theorems_diff;
2005-06-05 wenzelm 2005-06-05 File.shell_path;
2005-06-02 wenzelm 2005-06-02 tuned comment;
2005-05-23 wenzelm 2005-05-23 use: not a theory command!
2005-05-22 wenzelm 2005-05-22 string FindTheorems.criterion;
2005-05-22 wenzelm 2005-05-22 added print_simpset; renamed print_thms_containing to find_theorems; removed print_intros (superceded by find_theorems intro);
2005-05-17 wenzelm 2005-05-17 tuned;
2005-05-16 kleing 2005-05-16 searching for thms by combination of criteria (intro, elim, dest, name, term pattern)
2005-04-21 berghofe 2005-04-21 Adapted use command to new behaviour of Toplevel.node_trans
2005-04-13 wenzelm 2005-04-13 *** MESSAGE REFERS TO PREVIOUS VERSION *** Attrib.src; ISABELLE_DOC_FORMAT;
2005-04-13 wenzelm 2005-04-13 *** empty log message ***
2005-03-24 ballarin 2005-03-24 Further work on interpretation commands. New command `interpret' for interpretation in proof contexts.
2005-03-09 ballarin 2005-03-09 First version of global registration command.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2005-01-24 berghofe 2005-01-24 Specific theorems in a named list of theorems can now be referred to via indices (type thmref).
2004-10-11 berghofe 2004-10-11 Some changes to allow skipping of proof scripts.
2004-10-01 paulson 2004-10-01 display-drafts now uses pdf!
2004-09-27 ballarin 2004-09-27 Modified locales: improved implementation of "includes".
2004-08-12 ballarin 2004-08-12 Disallowed "includes" in locale declarations.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-06-15 wenzelm 2004-06-15 path instead of string;
2004-06-13 wenzelm 2004-06-13 added display_drafts and print_drafts commands;
2003-02-03 berghofe 2003-02-03 Moved print_intros from proof_general.ML to Isar/isar_cmd.ML
2002-07-02 wenzelm 2002-07-02 thms_containing: optional limit argument;
2002-07-02 wenzelm 2002-07-02 ProofContext.print_thms_containing;
2002-02-26 wenzelm 2002-02-26 markup commands: proper theory/proof transactions!
2002-02-25 wenzelm 2002-02-25 markup commands (from isar_thy.ML) with proper check of antiquotations;
2002-02-12 wenzelm 2002-02-12 got rid of explicit marginal comments (now stripped earlier from input);
2002-01-15 wenzelm 2002-01-15 print_locale: allow full body specification;
2001-12-05 wenzelm 2001-12-05 added print_rules;
2001-11-24 wenzelm 2001-11-24 print_locale: expr;
2001-11-09 berghofe 2001-11-09 Commands prf and full_prf can now also be used to display proof term of current proof state.