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

eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
Object_Logic.add_judgment more like Theory.specify_const;

HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015;
defs.ML: track dependencies also for type constructors;
typedef.ML: add type defined by typedef to dependencies, Abs and Rep now depend on the type;
Pure types and typedecls are final -- no dependencies;

trim context for persistent storage;

more explicit context;

tuned;

proper context for Object_Logic operations;

clarified Drule.gen_all: observe context more carefully;

tuned signature;

proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
clarified tool context in some boundary cases;

added Theory.setup convenience;

tuned signature;

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

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

modernized structure Proof_Context;

clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);

added merge_options convenience;

renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;

--HG--
rename : src/Pure/meta_simplifier.ML => src/Pure/raw_simplifier.ML

modernized some structure names, keeping a few legacy aliases;

renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;

separate structure Typedecl;

modernized structure Object_Logic;

discontinued unnamed infix syntax;

adapted Theory_Data;
tuned;

tuned message;

more uniform handling of binding in targets and derived elements;

removed Ids;

cleaned up binding module and related code

Drule.norm_hhf_eqs;

renamed iterated forall_conv to params_conv;

Context.>> : operate on Context.generic;

eliminated delayed theory setup

added base_sort;
added typedecl, dependent on base_sort (cf. intermediate typedecl.ML and former sign.ML, HOL/Tools/typedef_package.ML);
typedecl: recovered proper use of Syntax.type_name;

replaced obsolete Theory.add_finals_i by Theory.add_deps;

replaced literal 'a by Name.aT;

Conv.forall_conv: proper context;

renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;

tuned interfaces: atomize, atomize_prems, atomize_prems_tac;
removed atomize_cterm/goal;

avoid polymorphic equality;
added dest_judgment;

replaced HOLogic.Trueprop_conv by ObjectLogic.judgment_conv;

CONVERSION tactical;
MetaSimplifier.rewrite_goal_tac;

moved conversions to structure Conv;

simplified DataFun interfaces;

renamed some old names Theory.xxx to Sign.xxx;

reorganized structure Tactic vs. MetaSimplifier;

reorganized structure Goal vs. Tactic;

attribute: Context.mapping;
removed Drule.strip_shyps_warning;

added is_elim (from Provers/classical.ML);

tuned;

moved treatment of object-logic equalities to local_defs.ML;

removed unatomize;
added versions of meta_rewrite, unfold, fold;

renamed reverse_atomize to unatomize;
added rulify_term/tac;

tuned atomize_cterm;
added reverse_atomize_term/tac;

simplified type attribute;

setup: theory -> theory;

tuned;

forall_conv ~1;

renamed assert_prop to ensure_prop;

renamed atomize_rule to atomize_cterm;

accomodate change of TheoryDataFun;
accomodate identification of type Sign.sg and theory;
tuned;

tuned;

superceded by Pure.thy and CPure.thy;

Move towards standard functions.

Deleted Library.option type.

Moved conversion rules from MetaSimplifier to Drule. refl_implies removed
from Drule, instead imp_cong' exported from there.

Merged in license change from Isabelle2004

removed obsolete sort 'logic';

conversion of theorems to atomic form

Made judgments automatically declared final.

assert_propT;

added assert_judgment;

Changed interface of MetaSimplifier.rewrite_term.

full_atomize;

atomize_term replaces atomize_cterm;

added atomize_cterm;

renamed forall_elim_vars_safe to gen_all;

drop_judgment: be graceful about undeclared judgment;

tuned;

theory data: removed obsolete finish method;

theory data: finish method;

moved object_logic.ML to Isar/object_logic.ML;