tuned signature;

more explicit instantiate_morphism (without checks for typ / term component);

trim context of persistent data;
tuned signature;

prefer control symbol antiquotations;

store totality fact in function info

tuned;

support 'assumes' in specifications, e.g. 'definition', 'inductive';
tuned signatures;

tuned;

clarified bindings;

prefer binding over base name;

removed pointless check (see Type_Infer.object_logic);

trim context for persistent storage;
tuned signature;

have the installed termination prover take a 'quiet' flag

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

clarified context;

tuned signature -- prefer qualified names;

proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
occasionally clarified use of context;

just one data slot per program unit;
tuned signature;

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

tuned signature -- moved type src to Token, without aliases;

updated to named_theorems;
modernized module name and setup;

more antiquotations;

more qualified names;

maintain morphism names for diagnostic purposes;

qualifed popular user space names

generate elim rules for elimination of function equalities;
added fun_cases command;
recover proper cases rules for mutual recursive case (no sum types)

export dom predicate in the info record

export cases rule in the info record

added function store_termination_rule to the signature, as it is used in Nominal2

removed dead code;

proper signatures;

prefer formally checked @{keyword} parser;

discontinued Drule.term_rule, which tends to cause confusion due to builtin cterm_of (NB: the standard morphisms already provide a separate term component);

comments;

tuned Named_Thms: proper binding;

tuned signature -- refined terminology;

tuned Parse.group: delayed failure message;

modernized structure Proof_Context;

indentation;

removed support for tail-recursion from function package (now implemented by partial_function)

function (default) is legacy feature

tuned headers

improved error message for common mistake (fun f where "g x = ...")

turned show_sorts/show_types into proper configuration options;

more uniform descriptions, which end up in the collective output of 'print_attributes' for example;

theory data merge: prefer left side uniformly;

prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
eliminated old-style structure aliases K = Keyword, P = Parse;

prefer structure Parse_Spec;

farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)

default termination prover as plain tactic

new year's resolution: reindented code in function package

provide simp and induct rules in Function.info

more official data record Function.info

check if equations are present for all functions to avoid low-level exception later

adapted Generic_Data, Proof_Data;
tuned;

conceal partial rules depending on config flag (i.e. when called via "fun")

adapted Item_Net;
tuned;

configuration flag "partials"

function package: more standard names for structures and files