src/Pure/Isar/isar_cmd.ML
2008-03-19 ago renamed datatype thmref to Facts.ref, tuned interfaces;
2008-02-28 ago unused_thms: print via official context (ProofContext.pretty_fact),
2008-02-28 ago Added unused_thms command.
2008-02-15 ago tuned names;
2008-02-10 ago tuned default position;
2008-01-24 ago removed unused Toplevel.properties;
2008-01-03 ago nested_command: simplified properties vs. position -- the latter also includes id now;
2008-01-02 ago added nested_command (with explicit position argument via properties);
2007-11-07 ago Syntax.read_typ;
2007-10-09 ago generic Syntax.pretty/string_of operations;
2007-10-04 ago moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
2007-10-01 ago Simplified interface for printing of interpretations.
2007-09-08 ago thy_deps: ThyInfo.thy_ord, improved dir/unfold entry;
2007-09-01 ago replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
2007-08-17 ago removed obsolete touch_all_thys;
2007-08-07 ago theory loader: removed obsolete update_thy (coincides with use_thy);
2007-08-01 ago renamed 'print_options' to 'print_configs';
2007-07-30 ago marked some CRITICAL sections;
2007-07-28 ago type Morphism.declaration;
2007-07-28 ago tuned signature;
2007-07-27 ago renamed Config to ConfigOption;
2007-07-25 ago added command 'print_options';
2007-07-23 ago PrintMode.with_modes;
2007-07-22 ago simplified ThyInfo.begin_theory;
2007-07-19 ago removed obsolete use/update_thy_only;
2007-07-09 ago type output = string indicates raw system output;
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;