src/Pure/Isar/isar_cmd.ML
2005-05-23 ago use: not a theory command!
2005-05-22 ago string FindTheorems.criterion;
2005-05-22 ago added print_simpset;
2005-05-17 ago tuned;
2005-05-16 ago searching for thms by combination of criteria (intro, elim, dest, name, term pattern)
2005-04-21 ago Adapted use command to new behaviour of Toplevel.node_trans
2005-04-13 ago *** MESSAGE REFERS TO PREVIOUS VERSION ***
2005-04-13 ago *** empty log message ***
2005-03-24 ago Further work on interpretation commands. New command `interpret' for
2005-03-09 ago First version of global registration command.
2005-02-13 ago Deleted Library.option type.
2005-01-24 ago Specific theorems in a named list of theorems can now be referred to
2004-10-11 ago Some changes to allow skipping of proof scripts.
2004-10-01 ago display-drafts now uses pdf!
2004-09-27 ago Modified locales: improved implementation of "includes".
2004-08-12 ago Disallowed "includes" in locale declarations.
2004-06-21 ago Merged in license change from Isabelle2004
2004-06-15 ago path instead of string;
2004-06-13 ago added display_drafts and print_drafts commands;
2003-02-03 ago Moved print_intros from proof_general.ML to Isar/isar_cmd.ML
2002-07-02 ago thms_containing: optional limit argument;
2002-07-02 ago ProofContext.print_thms_containing;
2002-02-26 ago markup commands: proper theory/proof transactions!
2002-02-25 ago markup commands (from isar_thy.ML) with proper check of antiquotations;
2002-02-12 ago got rid of explicit marginal comments (now stripped earlier from input);
2002-01-15 ago print_locale: allow full body specification;
2001-12-05 ago added print_rules;
2001-11-24 ago print_locale: expr;
2001-11-09 ago Commands prf and full_prf can now also be used to display proof term
2001-11-06 ago print_syntax: include local version;
2001-11-06 ago added print_locales, print_locale;
2001-11-05 ago pretty/print functions with context;
2001-10-04 ago added print_induct_rules;
2001-08-31 ago Added functions for printing primitive proof terms.
2001-02-01 ago thms_containing: term args;
2000-12-04 ago dignostic commands: comment;
2000-08-29 ago pr: added prems limit;
2000-08-03 ago unknown_theory/proof/context;
2000-07-27 ago added thm_deps;
2000-07-06 ago allow comment in more commands;
2000-07-01 ago added print_trans_rules, print_antiquotations;
2000-06-25 ago rearranged print commands;
2000-05-31 ago transfer now automatic;
2000-05-18 ago print_state: flag for proof only;
2000-05-05 ago GPLed;
2000-03-17 ago kill: include kill_proof;
2000-03-15 ago pr: modes, optional limit;
2000-03-14 ago pr, disable_pr, enable_pr;
2000-03-08 ago added print_cases;
2000-03-06 ago moved use_mltext, use_mltext_theory, use_let, use_setup to context.ML;
1999-10-26 ago added kill_proof_notify;
1999-10-26 ago added kill_thy;
1999-10-21 ago added touch_child_thys;
1999-10-20 ago use_mltext: better control of verbosity;
1999-10-07 ago cd: quiet;
1999-10-05 ago replaced clear_undo by clear_undos;
1999-09-26 ago added print_thms_containing;
1999-09-07 ago read_typ/term: context_of;
1999-09-03 ago added welcome;
1999-09-01 ago removed kill_theory;