src/Pure/pure_thy.ML
2005-04-21 berghofe 2005-04-21 - Eliminated nodup_vars check. - Unification and matching functions now check types of term variables / sorts of type variables when applying a substitution. - Thm.instantiate now takes (ctyp * ctyp) list instead of (indexname * ctyp) list as argument, to allow for proper instantiation of theorems containing type variables with same name but different sorts.
2005-04-13 wenzelm 2005-04-13 *** MESSAGE REFERS TO PREVIOUS VERSION *** added datatype interval, improved thm selections;
2005-04-13 wenzelm 2005-04-13 *** empty log message ***
2005-04-11 ballarin 2005-04-11 First release of interpretation commands.
2005-03-24 ballarin 2005-03-24 Further work on interpretation commands. New command `interpret' for interpretation in proof contexts.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2005-02-10 berghofe 2005-02-10 Fixed bug in select_thm.
2005-02-10 berghofe 2005-02-10 Subscripts for theorem lists now start at 1.
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-12-08 nipkow 2004-12-08 fixed bug in find functions that I introduced some time ago.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-06-01 wenzelm 2004-06-01 removed obsolete sort 'logic';
2004-04-26 paulson 2004-04-26 commented
2004-04-14 wenzelm 2004-04-14 renamed have_thms to note_thms;
2004-02-11 berghofe 2004-02-11 Removed "duplicate fact binding" error message.
2003-10-09 skalberg 2003-10-09 Added support for making constants final, that is, ensuring that no definition can be given later (useful for constants whose behaviour is fixed axiomatically rather than definitionally).
2003-02-03 berghofe 2003-02-03 Moved find_intros_goal from goals.ML to pure_thy.ML
2002-11-13 berghofe 2002-11-13 Fixed name clash problem in forall_elim_var.
2002-10-21 berghofe 2002-10-21 Removed flexpair_def.
2002-10-14 nipkow 2002-10-14 Ported find_intro/elim to Isar.
2002-08-27 wenzelm 2002-08-27 disallow duplicate fact bindings for drafts (i.e. within new-style theory files);
2002-07-26 wenzelm 2002-07-26 tuned;
2002-07-02 wenzelm 2002-07-02 improved thms_containing (use FactIndex.T etc.);
2002-02-07 berghofe 2002-02-07 Theorems are only "pre-named" if the do not already have names.
2002-01-11 wenzelm 2002-01-11 have_thmss vs. have_thmss_i;
2002-01-10 wenzelm 2002-01-10 added hide_thms;
2001-11-28 wenzelm 2001-11-28 theory data: removed obsolete finish method;
2001-11-20 wenzelm 2001-11-20 trfuns *after* binder syntax;
2001-11-19 berghofe 2001-11-19 Further restructuring of theorem naming functions.
2001-11-11 wenzelm 2001-11-11 renamed open_smart_store_thms to smart_store_thms_open; added Syntax.pure_syntax_output;
2001-11-09 wenzelm 2001-11-09 theory data: finish method;
2001-10-31 berghofe 2001-10-31 - enter_thmx -> enter_thms - improved naming of theorems: enter_thms now takes functions pre_name and post_name as arguments
2001-09-28 wenzelm 2001-09-28 internal thm numbering with ":" instead of "_";
2001-08-31 berghofe 2001-08-31 Added equality axioms and initialization of proof term package.
2000-12-13 wenzelm 2000-12-13 eliminated GOAL syntax;
2000-11-12 wenzelm 2000-11-12 Syntax.pure_appl_syntax declared as output syntax for theory ProtoPure;
2000-09-17 wenzelm 2000-09-17 Display.pretty_thm_sg;
2000-09-02 wenzelm 2000-09-02 added get_thm_closure;
2000-08-09 wenzelm 2000-08-09 added get_thms_closure, single_thm;
2000-08-04 wenzelm 2000-08-04 dummy_pattern moved to term.ML;
2000-07-13 wenzelm 2000-07-13 add_defs(_i): overloaded option;
2000-07-04 wenzelm 2000-07-04 added "nothing" (empty list of theorems);
2000-07-01 wenzelm 2000-07-01 print_theorems: omit name space;
2000-06-29 wenzelm 2000-06-29 have_thmss: handle multiple lists of arguments;
2000-05-31 wenzelm 2000-05-31 get_thm(s): automatic transfer;
2000-04-17 wenzelm 2000-04-17 Pretty.chunks;
2000-03-13 wenzelm 2000-03-13 add_thms, add_axioms, add_defs: return theorems as well;
1999-11-29 wenzelm 1999-11-29 Goal: tuned pris;
1999-10-27 wenzelm 1999-10-27 dummy_pattern: aprop;
1999-10-21 wenzelm 1999-10-21 forall_elim_var(s) move here from drule.ML; add_axioms/defs: forall_elim_vars on result;
1999-10-08 wenzelm 1999-10-08 theorem database now also indexes constants "Trueprop", "all", "==>", "=="; thus thms_containing, findI etc. may retrieve more rules;
1999-10-06 wenzelm 1999-10-06 fixed naming of single axioms;
1999-09-06 wenzelm 1999-09-06 removed thms_closure (unused);
1999-09-04 wenzelm 1999-09-04 eliminated default_name (thms no longer stored for name "");
1999-09-01 wenzelm 1999-09-01 smart_store_thms;
1999-08-19 wenzelm 1999-08-19 tuned Goal syntax;
1999-07-12 wenzelm 1999-07-12 thms_containing: undeclared consts error;
1999-06-28 wenzelm 1999-06-28 cond_extern_table;
1999-06-04 wenzelm 1999-06-04 fixed BUG in have_thmss: return thy';