src/Pure/more_thm.ML
2012-09-01 wenzelm 2012-09-01 discontinued complicated/unreliable notion of recent proofs within context;
2012-08-31 wenzelm 2012-08-31 tuned signature;
2012-08-30 wenzelm 2012-08-30 some support for registering forked proofs within Proof.state, using its bottom context; tuned signature;
2012-08-30 wenzelm 2012-08-30 tuned signature;
2012-03-10 wenzelm 2012-03-10 eliminated dead code;
2012-03-07 wenzelm 2012-03-07 tuned signature;
2012-03-03 wenzelm 2012-03-03 canonical argument order for attribute application;
2012-02-15 wenzelm 2012-02-15 renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
2011-11-07 wenzelm 2011-11-07 made SML/NJ happy;
2011-11-06 wenzelm 2011-11-06 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute; misc tuning;
2011-07-12 wenzelm 2011-07-12 more uniform Properties in ML and Scala;
2011-06-09 wenzelm 2011-06-09 tuned signature: Name.invent and Name.invent_names;
2011-04-26 wenzelm 2011-04-26 mark thm tag "kind" as legacy;
2011-04-21 wenzelm 2011-04-21 discontinuend obsolete Thm.definitionK, which was hardly ever well-defined;
2011-04-17 wenzelm 2011-04-17 report Name_Space.declare/define, relatively to context; added "global" variants of context-dependent declarations;
2010-10-28 wenzelm 2010-10-28 type attribute is derived concept outside the kernel;
2010-09-05 wenzelm 2010-09-05 pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
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;