src/Pure/Isar/isar_cmd.ML
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.
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;