prefer control symbol antiquotations;

tuned signature;

tuned;

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

have the installed termination prover take a 'quiet' flag

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

clarified context;

just one data slot per program unit;
tuned signature;

modernized setup;

more antiquotations;

ported part of function package to new 'Ctr_Sugar' abstraction

proper signatures;

fun command: produce hard failure when equations do not contribute to the specification (i.e., are covered by preceding clauses), to avoid confusing inexperienced users

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

removed obsolete uses of Local_Theory.restore -- package composition P1 #> P2 no longer requires them due to 57def0b39696: P2 finds the results of P1 in the auxiliary context

less verbosity for 'function' and 'fun': observe "int" flag more carefully (cf. a32ca9165928);

export Function_Fun.fun_config for user convenience;

tuned signature: Name.invent and Name.invent_names;

prefer new-style Name.invents;

pervasive Output operations;

fun command produces warning when patterns are incomplete (somewhat analogous to primrec)

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

modernized structure Proof_Context;

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 = ...")

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

return updated info record after termination proof

clarified signature; simpler implementation in terms of function's tactic interface

default termination prover as plain tactic

ML interface uses plain command names, following conventions from typedef

new year's resolution: reindented code in function package

normalized uncurry take/drop

--HG--
extra : rebase_source : 647c8b5a6641f0eef6d4d81646474d16388f9fb9

curried take/drop

--HG--
extra : rebase_source : 6e6b508d936640bef00f0ad0c4fb089ad5253ef0

eliminated dead code and some unused bindings, reported by polyml

eliminated slightly odd name space grouping -- now managed by Isar toplevel;

modernized structure Local_Theory;

name space groups are identified by serial, not serial_string;

configuration flag "partials"

function package: more standard names for structures and files

renamed FundefDatatype -> Function_Fun