src/Pure/pure_thy.ML
2006-11-26 wenzelm 2006-11-26 updated (binder) syntax/notation;
2006-11-23 wenzelm 2006-11-23 tuned;
2006-11-21 wenzelm 2006-11-21 moved theorem kinds from PureThy to Thm; exported note_thms(s);
2006-10-04 haftmann 2006-10-04 *** empty log message ***
2006-09-21 wenzelm 2006-09-21 member (op =);
2006-07-11 wenzelm 2006-07-11 replaced Term.variant(list) by Name.variant(_list);
2006-07-08 wenzelm 2006-07-08 tuned exception handling;
2006-06-05 wenzelm 2006-06-05 support embedded terms;
2006-05-13 wenzelm 2006-05-13 added add_defs_unchecked(_i);
2006-05-05 wenzelm 2006-05-05 added syntax for _type_constraint_;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-04-26 wenzelm 2006-04-26 tuned;
2006-04-13 wenzelm 2006-04-13 moved print_theorems/theory to Isar/proof_display.ML;
2006-04-10 wenzelm 2006-04-10 Term.itselfT;
2006-03-21 wenzelm 2006-03-21 avoid polymorphic equality;
2006-02-22 wenzelm 2006-02-22 simplified Pure conjunction, based on actual const;
2006-02-15 wenzelm 2006-02-15 removed distinct, renamed gen_distinct to distinct;
2006-01-29 wenzelm 2006-01-29 proper order of trfuns;
2006-01-27 wenzelm 2006-01-27 moved theorem tags from Drule to PureThy; replaced kind attribute by kind string; tuned name_multi: index > 1 only; added note_thmss_qualified (from Isar/locale.ML);
2006-01-25 wenzelm 2006-01-25 export name_multi;
2006-01-21 wenzelm 2006-01-21 simplified type attribute;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory; added syntax (from Syntax/mixfix.ML); added HTML output syntax for _lambda;
2006-01-14 wenzelm 2006-01-14 sane ERROR handling;
2006-01-13 wenzelm 2006-01-13 generic_setup: optional argument, defaults to Context.setup();
2006-01-07 wenzelm 2006-01-07 gen_names: preserve empty names;
2005-12-16 haftmann 2005-12-16 re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-12-09 haftmann 2005-12-09 oriented result pairs in PureThy
2005-12-06 haftmann 2005-12-06 re-oriented some result tuples in PureThy
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.