2014-02-20 wenzelm 2014-02-20 clarified printing of undeclared hyps;
2014-02-17 wenzelm 2014-02-17 subtle change of semantics of Thm.eq_thm, e.g. relevant for merge of src/HOL/Tools/Predicate_Compile/core_data.ML (cf. HOL-IMP);
2014-01-11 wenzelm 2014-01-11 check_hyps when attributes are applied;
2014-01-11 wenzelm 2014-01-11 check_hyps for attribute application (still inactive, due to non-compliant tools); bypass check_hyps for locale expressions, where assumptions are not necessarily declared in intermediate situations;
2014-01-10 wenzelm 2014-01-10 more elementary management of declared hyps, below structure Assumption; Goal.prove: insist in declared hyps; Simplifier: declare hyps via Thm.assume_hyps; more accurate tool context in some boundary cases;
2013-08-26 wenzelm 2013-08-26 always transfer thm where attributes are applied -- relevant for internal 'notes' (e.g. via bundle 'includes') in contrast to external 'notes' (cf. Proof_Context.retrieve_thms);
2013-07-17 wenzelm 2013-07-17 more official Thm.eq_thm_strict, without demanding ML equality type;
2013-02-28 wenzelm 2013-02-28 discontinued empty name bindings in 'axiomatization';
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;