src/Pure/more_thm.ML
2010-05-08 wenzelm 2010-05-08 renamed Thm.get_name -> Thm.derivation_name and Thm.put_name -> Thm.name_derivation, to emphasize the true nature of these operations;
2010-04-11 wenzelm 2010-04-11 Thm.add_axiom/add_def: return internal name of foundational axiom;
2010-03-27 wenzelm 2010-03-27 disallow premises in primitive Theory.add_def -- handle in Thm.add_def; eliminated obsolete Sign.cert_def; misc tuning and clarification;
2010-03-27 wenzelm 2010-03-27 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML); discontinued old-style Theory.add_defs(_i) in favour of more basic Theory.add_def; modernized PureThy.add_defs etc. -- refer to high-level Thm.add_def;
2010-03-22 wenzelm 2010-03-22 replaced Theory.add_axioms(_i) by more primitive Theory.add_axiom;
2010-03-21 wenzelm 2010-03-21 add_axiom: axiomatize "unconstrained" version, with explicit of_class premises; more uniform add_axiom/add_def;
2010-03-21 wenzelm 2010-03-21 more explicit invented name;
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-03-11 wenzelm 2010-03-11 tuned;
2010-02-27 wenzelm 2010-02-27 modernized structure Term_Ord;
2010-02-19 wenzelm 2010-02-19 Thm.def_binding;
2009-11-16 wenzelm 2009-11-16 eliminated obsolete thm position stuff;
2009-11-15 wenzelm 2009-11-15 tuned;
2009-11-13 wenzelm 2009-11-13 eliminated obsolete "generated" kind -- collapsed to unspecific "" (definitely unused according to Lukas Bulwahn);
2009-11-12 wenzelm 2009-11-12 eliminated slightly odd (unused) "axiom" and "assumption" -- collapsed to unspecific "";
2009-11-12 wenzelm 2009-11-12 eliminated obsolete "internal" kind -- collapsed to unspecific "";
2009-11-05 wenzelm 2009-11-05 scalable version of Named_Thms, using Item_Net;
2009-11-01 wenzelm 2009-11-01 adapted Item_Net; tuned;
2009-10-29 wenzelm 2009-10-29 eliminated obsolete/unused Thm.kind_internal/is_internal etc.;
2009-10-25 wenzelm 2009-10-25 maintain group via name space, not tags;
2009-10-01 wenzelm 2009-10-01 added Ctermtab, cterm_cache, thm_cache; tuned;
2009-07-30 wenzelm 2009-07-30 added certify_inst, certify_instantiate;
2009-07-26 wenzelm 2009-07-26 lambda/cabs/all: named variants;
2009-07-09 wenzelm 2009-07-09 renamed structure TermSubst to Term_Subst;
2009-07-09 wenzelm 2009-07-09 renamed functor TableFun to Table, and GraphFun to Graph;
2009-07-06 wenzelm 2009-07-06 clarified strip_shyps: proper type witnesses for present sorts; moved fold_terms to thm.ML;
2009-07-06 wenzelm 2009-07-06 clarified Thm.of_class/of_sort/class_triv;
2009-07-02 wenzelm 2009-07-02 renamed Drule.sort_triv to Thm.sort_triv (cf. more_thm.ML);
2009-05-18 haftmann 2009-05-18 introduced Thm.generatedK
2009-05-16 bulwahn 2009-05-16 added new kind generated_theorem for theorems which are generated by packages to distinguish between theorems from users and packages
2009-03-17 wenzelm 2009-03-17 tuned comment;
2009-03-17 wenzelm 2009-03-17 adapted to general Item_Net;
2009-03-11 wenzelm 2009-03-11 added def_binding_optional -- robust version of def_name_optional for bindings;
2009-03-07 wenzelm 2009-03-07 moved Thm.def_name(_optional) to more_thm.ML; moved old-style Thm.get_def to Drule.get_def;
2009-03-03 wenzelm 2009-03-03 added type binding and val empty_binding;
2009-01-21 haftmann 2009-01-21 binding replaces bstring
2008-12-31 wenzelm 2008-12-31 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-10-23 wenzelm 2008-10-23 renamed Thm.get_axiom_i to Thm.axiom;
2008-10-16 wenzelm 2008-10-16 added check_shyps, which reject pending sort hypotheses;
2008-09-03 wenzelm 2008-09-03 simplified add_axiom: no hyps;
2008-08-27 wenzelm 2008-08-27 type Properties.T;
2008-08-14 wenzelm 2008-08-14 moved basic thm operations from structure PureThy to Thm; added position operations; tuned;
2008-06-18 wenzelm 2008-06-18 removed obsolete read_def_cterms/read_cterm;
2008-04-15 wenzelm 2008-04-15 Theory.eq_thy;
2008-04-15 wenzelm 2008-04-15 Thm.forall_elim_var(s);
2008-04-12 wenzelm 2008-04-12 replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
2007-12-03 haftmann 2007-12-03 interface for unchecked definitions
2007-10-11 wenzelm 2007-10-11 added elim_implies (more convenient argument order); added unvarify (from drule.ML); added specification primitives: add_axiom, add_def;
2007-10-10 wenzelm 2007-10-10 tuned;
2007-09-30 wenzelm 2007-09-30 Markup.internalK;
2007-07-29 wenzelm 2007-07-29 moved Drule.add/del/merge_rules to Thm.add/del/merge_thms; moved Drule.is_dummy_thm to Thm.is_dummy;
2007-07-05 wenzelm 2007-07-05 added is_reflexive;
2007-06-25 wenzelm 2007-06-25 added reasonably efficient add_cterm_frees;
2007-05-31 wenzelm 2007-05-31 made aconvc pervasive;
2007-05-31 wenzelm 2007-05-31 moved aconvc to more_thm.ML;
2007-05-10 wenzelm 2007-05-10 added destructors from drule.ML; added mk_binop;
2007-04-15 wenzelm 2007-04-15 moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
2007-04-14 wenzelm 2007-04-14 added read_def_cterms, read_cterm (from thm.ML);
2007-02-28 wenzelm 2007-02-28 tuned;