src/Pure/Isar/isar_cmd.ML
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.
2001-11-06 wenzelm 2001-11-06 print_syntax: include local version;
2001-11-06 wenzelm 2001-11-06 added print_locales, print_locale;
2001-11-05 wenzelm 2001-11-05 pretty/print functions with context;
2001-10-04 wenzelm 2001-10-04 added print_induct_rules;
2001-08-31 berghofe 2001-08-31 Added functions for printing primitive proof terms.
2001-02-01 wenzelm 2001-02-01 thms_containing: term args;
2000-12-04 wenzelm 2000-12-04 dignostic commands: comment;
2000-08-29 wenzelm 2000-08-29 pr: added prems limit;
2000-08-03 wenzelm 2000-08-03 unknown_theory/proof/context;
2000-07-27 wenzelm 2000-07-27 added thm_deps;
2000-07-06 wenzelm 2000-07-06 allow comment in more commands;
2000-07-01 wenzelm 2000-07-01 added print_trans_rules, print_antiquotations;
2000-06-25 wenzelm 2000-06-25 rearranged print commands;
2000-05-31 wenzelm 2000-05-31 transfer now automatic;
2000-05-18 wenzelm 2000-05-18 print_state: flag for proof only;
2000-05-05 wenzelm 2000-05-05 GPLed;
2000-03-17 wenzelm 2000-03-17 kill: include kill_proof;
2000-03-15 wenzelm 2000-03-15 pr: modes, optional limit; print_thms/prop/term/type: modes;
2000-03-14 wenzelm 2000-03-14 pr, disable_pr, enable_pr;
2000-03-08 wenzelm 2000-03-08 added print_cases;
2000-03-06 wenzelm 2000-03-06 moved use_mltext, use_mltext_theory, use_let, use_setup to context.ML;
1999-10-26 wenzelm 1999-10-26 added kill_proof_notify;
1999-10-26 wenzelm 1999-10-26 added kill_thy;
1999-10-21 wenzelm 1999-10-21 added touch_child_thys;
1999-10-20 wenzelm 1999-10-20 use_mltext: better control of verbosity;
1999-10-07 wenzelm 1999-10-07 cd: quiet;
1999-10-05 wenzelm 1999-10-05 replaced clear_undo by clear_undos;
1999-09-26 wenzelm 1999-09-26 added print_thms_containing; use_mltext: strictly diag;
1999-09-07 wenzelm 1999-09-07 read_typ/term: context_of;
1999-09-03 wenzelm 1999-09-03 added welcome;
1999-09-01 wenzelm 1999-09-01 removed kill_theory; print_thms: use Proof.pretty_thms;
1999-08-20 wenzelm 1999-08-20 print_context;
1999-07-28 wenzelm 1999-07-28 added pretty_setmargin;
1999-07-27 wenzelm 1999-07-27 removed restart; added touch_all_thys, touch_thy, remove_thy, update_thy_only;
1999-07-16 wenzelm 1999-07-16 removed break;
1999-07-15 wenzelm 1999-07-15 improved print_thms;
1999-05-27 wenzelm 1999-05-27 improved undo / kill operations;
1999-05-26 wenzelm 1999-05-26 cannot_undo;
1999-05-21 wenzelm 1999-05-21 added use_thy_only;
1999-05-21 wenzelm 1999-05-21 history commands;
1999-05-17 wenzelm 1999-05-17 node_cases renamed to node_case;
1999-05-11 wenzelm 1999-05-11 fixed msg;
1999-02-08 wenzelm 1999-02-08 use: provide context;
1999-02-05 wenzelm 1999-02-05 use_thy, update_thy: Context.save;
1999-02-04 wenzelm 1999-02-04 File.pwd, File.cd;
1999-02-03 wenzelm 1999-02-03 removed load; proper use (ThyInfo.load_file); added use_thy, update_thy;
1999-01-12 wenzelm 1999-01-12 eliminated tthm type and Attribute structure;