tuned -- avoid spurious exception trace for "the";

eliminated somewhat pointless parallelism (from 857da80611ab): usually hundreds of tasks with < 1ms each, also note that the enclosing join_theory happens within theory graph parallelism;

prefer symbols;

eliminated ASCII syntax from Pure bootstrap;
tuned comments;

explicit operations to instantiate frees: typ, term, thm, morphism;

support for lazy notes in global/local context and Element.Lazy_Notes: name binding and fact without attributes;
register_proofs is now based on lazy thms, but Thm.consolidate_theory will eventually force this (in parallel);
support for lazy notes for locale activation (still inactive);

tuned signature;

clarified signature;

consolidate proofs more simultaneously;

tuned signature;

consolidate nested thms with persistent result, for improved performance;
always consolidate parts of fulfill_norm_proof: important to exhibit cyclic thms (via non-termination as officially published), but this was lost in f33d5a00c25d;

more careful derivation_closed / close_derivation;

more symbols;

tuned signature;

clarified def binding position: reset for implicit/derived binding, keep for explicit binding;

more uniform treatment of package internals;

rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;

tuned signature -- clarified modules;

print thm wrt. local shyps (from full proof context);
tuned;

clarified modules;
tuned signature;

added Thm.forall_intr_name;

just one theorem kind, which is legacy anyway;

moved remaining display.ML to more_thm.ML;

tuned;

tuned signature: eliminated pointless type Context.pretty;

more explicit Defs.context: use proper name spaces as far as possible;

trim context for persistent storage;

tuned;

tuned;

tuned signature;

produce certified vars without access to theory_of_thm, and without context;

produce certified vars without access to theory_of_thm, and without context;

tuned;

prefer theory_id operations;
tuned signature;

clarified context;

more explicit context;
tuned signature;

eliminated dead code;

more direct access to atomic cterms;

proper context;

more direct access to atomic cterms;

clarified context;

tuned signature;
clarified context;

tuned signature;

simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);

clarified context;

tuned;

explicitly checked alpha conversion -- actual renaming happens outside kernel;

clarified context;

Thm.cterm_of and Thm.ctyp_of operate on local context;

tuned -- more explicit use of context;

clarified signature;

tuned signature -- prefer qualified names;

renamed "pairself" to "apply2", in accordance to @{apply 2};

more general dummy: may contain "parked arguments", for example;

more qualified names;

clarified printing of undeclared hyps;

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);

check_hyps when attributes are applied;

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;

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;

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);

more official Thm.eq_thm_strict, without demanding ML equality type;

discontinued empty name bindings in 'axiomatization';

discontinued complicated/unreliable notion of recent proofs within context;

tuned signature;

some support for registering forked proofs within Proof.state, using its bottom context;
tuned signature;

tuned signature;

eliminated dead code;

tuned signature;

canonical argument order for attribute application;

renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;

made SML/NJ happy;

more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
misc tuning;

more uniform Properties in ML and Scala;

tuned signature: Name.invent and Name.invent_names;

mark thm tag "kind" as legacy;

discontinuend obsolete Thm.definitionK, which was hardly ever well-defined;

report Name_Space.declare/define, relatively to context;
added "global" variants of context-dependent declarations;

type attribute is derived concept outside the kernel;

pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;

renamed Thm.get_name -> Thm.derivation_name and Thm.put_name -> Thm.name_derivation, to emphasize the true nature of these operations;

Thm.add_axiom/add_def: return internal name of foundational axiom;

disallow premises in primitive Theory.add_def -- handle in Thm.add_def;
eliminated obsolete Sign.cert_def;
misc tuning and clarification;

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;

replaced Theory.add_axioms(_i) by more primitive Theory.add_axiom;

add_axiom: axiomatize "unconstrained" version, with explicit of_class premises;
more uniform add_axiom/add_def;

more explicit invented name;

renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;

tuned;

modernized structure Term_Ord;

Thm.def_binding;

eliminated obsolete thm position stuff;

tuned;

eliminated obsolete "generated" kind -- collapsed to unspecific "" (definitely unused according to Lukas Bulwahn);

eliminated slightly odd (unused) "axiom" and "assumption" -- collapsed to unspecific "";

eliminated obsolete "internal" kind -- collapsed to unspecific "";

scalable version of Named_Thms, using Item_Net;

adapted Item_Net;
tuned;

eliminated obsolete/unused Thm.kind_internal/is_internal etc.;

maintain group via name space, not tags;

added Ctermtab, cterm_cache, thm_cache;
tuned;

added certify_inst, certify_instantiate;

lambda/cabs/all: named variants;

renamed structure TermSubst to Term_Subst;

renamed functor TableFun to Table, and GraphFun to Graph;

clarified strip_shyps: proper type witnesses for present sorts;
moved fold_terms to thm.ML;

clarified Thm.of_class/of_sort/class_triv;

renamed Drule.sort_triv to Thm.sort_triv (cf. more_thm.ML);

introduced Thm.generatedK

added new kind generated_theorem for theorems which are generated by packages to distinguish between theorems from users and packages

tuned comment;

adapted to general Item_Net;

added def_binding_optional -- robust version of def_name_optional for bindings;

moved Thm.def_name(_optional) to more_thm.ML;
moved old-style Thm.get_def to Drule.get_def;

Merge.

added type binding and val empty_binding;

binding replaces bstring

moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
tuned signature of structure Term;

cleaned up binding module and related code

renamed Thm.get_axiom_i to Thm.axiom;

added check_shyps, which reject pending sort hypotheses;

simplified add_axiom: no hyps;

type Properties.T;

moved basic thm operations from structure PureThy to Thm;
added position operations;
tuned;

removed obsolete read_def_cterms/read_cterm;

Theory.eq_thy;

Thm.forall_elim_var(s);

replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);

interface for unchecked definitions

added elim_implies (more convenient argument order);
added unvarify (from drule.ML);
added specification primitives: add_axiom, add_def;

tuned;

Markup.internalK;

moved Drule.add/del/merge_rules to Thm.add/del/merge_thms;
moved Drule.is_dummy_thm to Thm.is_dummy;

added is_reflexive;

added reasonably efficient add_cterm_frees;

made aconvc pervasive;

moved aconvc to more_thm.ML;

added destructors from drule.ML;
added mk_binop;

moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;

added read_def_cterms, read_cterm (from thm.ML);

tuned;

Further operations on type thm, outside the inference kernel.