src/Pure/Isar/isar_cmd.ML
2007-05-08 wenzelm 2007-05-08 tuned ProofDisplay.pretty_full_theory;
2007-04-05 wenzelm 2007-04-05 thy_deps: sort Context.thy_ord;
2007-04-04 wenzelm 2007-04-04 simplified thy_deps using Theory.ancestors_of (in order of creation);
2007-04-03 wenzelm 2007-04-03 avoid clash with Alice keywords;
2007-03-20 haftmann 2007-03-20 added theory dependency graph
2007-02-20 kleing 2007-02-20 Remove duplicates from printed theorems in find_theorems (still pretty slow, needs optimising). Added syntax "find_theorems (..) with_dups .." to switch off removal.
2007-02-04 wenzelm 2007-02-04 tuned oracle interface; simproc_setup: added identifier;
2007-01-28 wenzelm 2007-01-28 added simproc_setup;
2007-01-19 wenzelm 2007-01-19 added various ML setup functions (from sign.ML, pure_thy.ML);
2007-01-19 wenzelm 2007-01-19 added 'declaration' command; adapted ML context operations;
2006-12-30 wenzelm 2006-12-30 removed obsolete clear_undos_theory; undo/cannot_undo: proper undo of 'end';
2006-12-29 wenzelm 2006-12-29 removed obsolete init_context;
2006-12-15 wenzelm 2006-12-15 avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
2006-12-09 wenzelm 2006-12-09 added print_abbrevs; exit: less verbosity;
2006-12-05 wenzelm 2006-12-05 print_syntax etc.: plain Toplevel.context_of;
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!