added HOLogic.mk_obj_eq convenience and eliminated some clones;

prefer control symbol antiquotations;

more general signature; works for all terms, not just frees

tuned signature;

clarified bindings;

clarified bindings;

prefer binding over base name;

prefer precise names for internal construction;

more uniform treatment of package internals;

avoid hardwired frees;
tuned;

do not expose low-level "_def" facts of 'function' definitions, to avoid potential confusion with the situation of plain 'definition';

tuned signature;

prefer tactics with explicit context;

clarified context;

clarified role of naming for background theory: transform_binding (e.g. for "concealed" flag) uses naming of hypothetical context;

tuned signature;

clarified context;

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

clarified context;

tuned signature -- prefer qualified names;

eliminated some clones of Proof_Context.cterm_of

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

proper context for assume_tac (atac remains as fall-back without context);

optional proof context for unify operations, for the sake of proper local options;

modernized setup;
more standard module name;

--HG--
rename : src/HOL/Tools/Function/context_tree.ML => src/HOL/Tools/Function/function_context_tree.ML

added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};

more antiquotations;

got rid of dynamic scoping the easy way

moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain

--HG--
rename : src/HOL/FunDef.thy => src/HOL/Fun_Def.thy

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

tuned signature;

tuned signature;

export dom predicate in the info record

tuned signature -- more explicit flags for low-level Thm.bicompose;

simplifier uses proper Proof.context instead of historic type simpset;

discontinued obsolete fork_mono to loosen some brakes -- NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;

renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const;

proper Proof.context for classical tactics;
reduced claset to snapshot of classical context;
discontinued clasimpset;

eliminated obsolete Function_Lib.frees_in_term;
simplified;

observe firm naming convention ctxt: Proof.context;

modernized structure Proof_Context;

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

function (default) is legacy feature

tuned headers

eliminated aliases of Type.constraint;

more permissive: simplification solves the goal when rhs = undefined

tuned quotes

use antiquotations for remaining unqualified constants in HOL

renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;

less pervasive names from structure Thm;

incorporated further conversions and conversionals, after some minor tuning;

tolerate eta-variants in f_graph.cases (from inductive package); added test case;

new year's resolution: reindented code in function package

moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)

eliminated dead code and some unused bindings, reported by polyml

adapted Local_Theory.define -- eliminated odd thm kind;

modernized structure Local_Theory;

inductive: eliminated obsolete kind;

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

less verbose inductive invocation

tuned

absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned

conceal internal bindings;

function package: more standard names for structures and files