2005-03-24 ago Further work on interpretation commands. New command `interpret' for
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2005-02-10 ago Fixed bug in select_thm.
2005-02-10 ago Subscripts for theorem lists now start at 1.
2005-01-24 ago Specific theorems in a named list of theorems can now be referred to
2004-12-08 ago fixed bug in find functions that I introduced some time ago.
2004-06-21 ago Merged in license change from Isabelle2004
2004-06-01 ago removed obsolete sort 'logic';
2004-04-26 ago commented
2004-04-14 ago renamed have_thms to note_thms;
2004-02-11 ago Removed "duplicate fact binding" error message.
2003-10-09 ago Added support for making constants final, that is, ensuring that no
2003-02-03 ago Moved find_intros_goal from goals.ML to pure_thy.ML
2002-11-13 ago Fixed name clash problem in forall_elim_var.
2002-10-21 ago Removed flexpair_def.
2002-10-14 ago Ported find_intro/elim to Isar.
2002-08-27 ago disallow duplicate fact bindings for drafts (i.e. within new-style theory files);
2002-07-26 ago tuned;
2002-07-02 ago improved thms_containing (use FactIndex.T etc.);
2002-02-07 ago Theorems are only "pre-named" if the do not already have names.
2002-01-11 ago have_thmss vs. have_thmss_i;
2002-01-10 ago added hide_thms;
2001-11-28 ago theory data: removed obsolete finish method;
2001-11-20 ago trfuns *after* binder syntax;
2001-11-19 ago Further restructuring of theorem naming functions.
2001-11-11 ago renamed open_smart_store_thms to smart_store_thms_open;
2001-11-09 ago theory data: finish method;
2001-10-31 ago - enter_thmx -> enter_thms
2001-09-28 ago internal thm numbering with ":" instead of "_";
2001-08-31 ago Added equality axioms and initialization of proof term package.
2000-12-13 ago eliminated GOAL syntax;
2000-11-12 ago Syntax.pure_appl_syntax declared as output syntax for theory ProtoPure;
2000-09-17 ago Display.pretty_thm_sg;
2000-09-02 ago added get_thm_closure;
2000-08-09 ago added get_thms_closure, single_thm;
2000-08-04 ago dummy_pattern moved to term.ML;
2000-07-13 ago add_defs(_i): overloaded option;
2000-07-04 ago added "nothing" (empty list of theorems);
2000-07-01 ago print_theorems: omit name space;
2000-06-29 ago have_thmss: handle multiple lists of arguments;
2000-05-31 ago get_thm(s): automatic transfer;
2000-04-17 ago Pretty.chunks;
2000-03-13 ago add_thms, add_axioms, add_defs: return theorems as well;
1999-11-29 ago Goal: tuned pris;
1999-10-27 ago dummy_pattern: aprop;
1999-10-21 ago forall_elim_var(s) move here from drule.ML;
1999-10-08 ago theorem database now also indexes constants "Trueprop", "all",
1999-10-06 ago fixed naming of single axioms;
1999-09-06 ago removed thms_closure (unused);
1999-09-04 ago eliminated default_name (thms no longer stored for name "");
1999-09-01 ago smart_store_thms;
1999-08-19 ago tuned Goal syntax;
1999-07-12 ago thms_containing: undeclared consts error;
1999-06-28 ago cond_extern_table;
1999-06-04 ago fixed BUG in have_thmss: return thy';
1999-05-21 ago avoid string constants;
1999-05-21 ago backup replaced by checkpoint;
1999-05-17 ago backup operation replaces transaction;
1999-05-04 ago transaction: Theory.copy;