tuned signature;

prefer control symbol antiquotations;

clarified signature: proper result;

clarified signature: proper result;

clarified syntax;

allow 'for' fixes for multi_specs;

tuned proofs, to allow unfold_abs_def;

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

avoid clash with function called "x";

clarified bindings;

clarified signature;

clarified reported positions;

operate on proper binding;
tuned;

eliminated "xname" and variants;

more uniform treatment of package internals;

tuned signature;

more general types Proof.method / context_tactic;
proper context for Method.insert_tac;
tuned;

prod_case as canonical name for product type eliminator

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

trim context for persistent storage;

updated to infer_instantiate;

Variable.focus etc.: optional bindings provided by user;
Subgoal.focus command: more careful treatment of user-provided bindings;

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

@{command_spec} is superseded by @{command_keyword};

tuned signature;

Thm.cterm_of and Thm.ctyp_of operate on local 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;

eliminated aliases;

updated to named_theorems;
modernized module name and setup;

proper context for norm_hhf and derived operations;
clarified tool context in some boundary cases;

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

restrict admissibility to non-empty chains to allow more syntax-directed proof rules

ported 'partial_function' to 'Ctr_Sugar' abstraction

derive specialized version of full fixpoint induction (with admissibility)

export mono_thm

more robust instantiation: extract vars from conclusion instead of relying on fixed overall ordering

more precise treatment of theory vs. Proof.context;

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

allow induction predicates with arbitrary arity (not just binary)

outer syntax command definitions based on formal command_spec derived from theory header declarations;

prefer formally checked @{keyword} parser;

tuned;

tuned Named_Thms: proper binding;

match types when applying mono_thm -- previous export generalizes type variables;
added trivial regression test

generate raw induction rule as instance of generic rule with careful treatment of currying

also manage induction rule;
tuned data slot

separate initializations for different modes of partial_function -- generation of induction rules will be non-uniform

clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;

standardized aliases of operations on tsig;

modernized structure Proof_Context;

added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;

misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;

eliminated dest_all_all_ctx

partial_function is a declaration command

fixed confusion introduced in 008dc2d2c395

added Spec_Rule declaration to partial_function

declare recursive equation as ".simps", in accordance with other packages

first version of partial_function package