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;
1999-08-20 ago print_context;
1999-07-28 ago added pretty_setmargin;
1999-07-27 ago removed restart;
1999-07-16 ago removed break;
1999-07-15 ago improved print_thms;
1999-05-27 ago improved undo / kill operations;
1999-05-26 ago cannot_undo;
1999-05-21 ago added use_thy_only;