tuned signature;

tuned signature (again);

trim context of persistent data;
tuned signature;

prefer control symbol antiquotations;

proper concept of code declaration wrt. atomicity and Isar declarations

--HG--
extra : rebase_source : adb08da85e01b6c9c81d471a0d8e7ebb68d7e472

store totality fact in function info

explicit tagging of code equations de-baroquifies interface

--HG--
extra : rebase_source : 1d83d31f669dc30b586df508a64fdc3a9e7b2655

tuned;

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

prefer internal attribute source;

clarified bindings;

clarified bindings;

clarified bindings;

prefer binding over base name;

tuned;

Type_Infer.object_logic controls improvement of type inference result;

reconcile object-logic constraint vs. mixfix constraint;

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

trim context for persistent storage;
tuned signature;

clarified context;

avoid dynamic parsing of hardwired strings;

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

tuned signature;

tuned signature -- prefer qualified names;

just one data slot per program unit;
tuned signature;

modernized setup;

modernized setup;
more standard module name;

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

renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place

--HG--
rename : src/HOL/Datatype.thy => src/HOL/Old_Datatype.thy
rename : src/HOL/Tools/Function/size.ML => src/HOL/Tools/Function/old_size.ML
rename : src/HOL/Tools/Datatype/datatype.ML => src/HOL/Tools/Old_Datatype/old_datatype.ML
rename : src/HOL/Tools/Datatype/datatype_aux.ML => src/HOL/Tools/Old_Datatype/old_datatype_aux.ML
rename : src/HOL/Tools/Datatype/datatype_codegen.ML => src/HOL/Tools/Old_Datatype/old_datatype_codegen.ML
rename : src/HOL/Tools/Datatype/datatype_data.ML => src/HOL/Tools/Old_Datatype/old_datatype_data.ML
rename : src/HOL/Tools/Datatype/datatype_prop.ML => src/HOL/Tools/Old_Datatype/old_datatype_prop.ML
rename : src/HOL/Tools/Datatype/datatype_realizer.ML => src/HOL/Tools/Old_Datatype/old_datatype_realizer.ML
rename : src/HOL/Tools/Datatype/primrec.ML => src/HOL/Tools/Old_Datatype/old_primrec.ML
rename : src/HOL/Tools/Datatype/rep_datatype.ML => src/HOL/Tools/Old_Datatype/old_rep_datatype.ML

updated to named_theorems;
modernized module name and setup;

more position markup to help locating the query context, e.g. from "Info" dockable;

more antiquotations;

transformed 'option' and 'list' into new-style datatypes (but register them as old-style as well)
* * *
compile
* * *
tuned imports to prevent merge issues in 'Main'

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

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

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

omit automatic Induct.cases_pred declaration, which breaks many existing proofs

clarified

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

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

prefer negative "consumes", relative to the total number of prems, which is stable under more morphisms, notably those from nested context with assumes (cf. existing treatment of 'obtains');

recovered explicit error message, which was lost in b8570ea1ce25;

more precise indentation;

more standard method setup;

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

added ML antiquotation @{attributes};

uniform Local_Theory.declaration with explicit params;

tuned signature -- refined terminology;

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

less verbosity in batch mode -- spam reduction and notable performance improvement;
clarified Proof_Display.print_consts;

slightly more uniform messages;

pervasive Output operations;

modernized structure Proof_Context;

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

function (default) is legacy feature

function (tailrec) is a legacy feature

tuned headers

some cleanup in Function_Lib

no longer declare .psimps rules as [simp].

This regularly caused confusion (e.g., they show up in simp traces
when the regular simp rules are disabled). In the few places where the
rules are used, explicitly mentioning them actually clarifies the
proof text.

tuned titles

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

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

return updated info record after termination proof

return info record (relative to auxiliary context!)

function: sane interface for programmatic use

ML interface uses plain command names, following conventions from typedef

function: better separate Isar integration from actual functionality

modernized naming conventions of main Isar proof elements;

refining and adding Spec_Rules to definitional packages old_primrec, primrec, recdef, size and function

more antiquotations;

adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening

function package: declare Spec_Rules for simps from total functions, but not psimps or tail-rec equations

new year's resolution: reindented code in function package

provide simp and induct rules in Function.info

more official data record Function.info

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

modernized structure Local_Theory;

eliminated slightly odd kind argument of LocalTheory.note(s);
added LocalTheory.notes_kind as fall-back for unusual cases;

eliminated obsolete "generated" kind -- collapsed to unspecific "" (definitely unused according to Lukas Bulwahn);

removed unused Quickcheck_RecFun_Simps;

adapted LocalTheory.declaration;

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

conceal "termination" rule, used only by special tools

modernized structure Context_Rules;

modernized structure Rule_Cases;

name space groups are identified by serial, not serial_string;

configuration flag "partials"

function package: more standard names for structures and files