src/Pure/pure_thy.ML
2005-10-28 wenzelm 2005-10-28 datatype thmref: added Fact; renamed Goal constant to prop;
2005-10-19 wenzelm 2005-10-19 added thm(s) retrieval functions (from goals.ML);
2005-09-29 wenzelm 2005-09-29 Theory.add_finals_i;
2005-09-20 haftmann 2005-09-20 slight adaptions to library changes
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update; add_defs etc.: use Thm.get_axiom_i, which is independent from naming;
2005-09-13 wenzelm 2005-09-13 added generic_setup, add_oracle (from isar_thy.ML);
2005-09-01 wenzelm 2005-09-01 curried_lookup/update;
2005-08-28 wenzelm 2005-08-28 export theorems_of;
2005-08-01 wenzelm 2005-08-01 Compress.init_data;
2005-07-13 haftmann 2005-07-13 (intermediate commit)
2005-07-06 wenzelm 2005-07-06 tuned forall_elim_var(s): avoid expensive Term.add_vars;
2005-06-22 wenzelm 2005-06-22 renamed init to init_data;
2005-06-21 wenzelm 2005-06-21 enter_thms: use theorem database of thy *after* attribute application;
2005-06-20 wenzelm 2005-06-20 datatype thmref = Name ... | NameSelection ...; added print_theorems_diff; tuned;
2005-06-17 wenzelm 2005-06-17 added theorem_space; removed unused extern_thm_sg; accomodate change of TheoryDataFun; accomodate identification of type Sign.sg and theory; removed theory management (cf. 'history' in context.ML); moved add_typedecls to sign.ML; Sign.init, Theory.init; tuned;
2005-06-09 wenzelm 2005-06-09 thms_of no longer global; added all_thms_of; theorems: NameSpace.table;
2005-05-31 wenzelm 2005-05-31 renamed cond_extern to extern; removed note_thmss_accesses(_i) -- functionality covered by general naming context;
2005-05-22 wenzelm 2005-05-22 added string_of_thmref, selections, fact_index_of, valid_thms; moved find_matching_thms, is_matching_thm, find_intros/intros_goal/elims to Isar/find_theorems.ML; tuned
2005-05-17 wenzelm 2005-05-17 moved credit to CONTRIBUTORS;
2005-05-16 kleing 2005-05-16 searching for thms by combination of criteria (intro, elim, dest, name, term pattern)
2005-04-29 kleing 2005-04-29 credits
2005-04-29 kleing 2005-04-29 new thms_containing that searches for patterns instead of constants (by Rafal Kolanski, NICTA)
2005-04-21 wenzelm 2005-04-21 superceded by Pure.thy and CPure.thy;
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;