isabelle update -u control_cartouches;

compactified output

implicit eta contraction for preprocessed terms avoids unintended implicit eta expansion

optional timing for code generator conversions

corrected closure scope of static_conv_thingol;
clarified implementation and names

clarified naming conventions and code for code evaluation sandwiches

clarified context, notably for internal use of Simplifier;

provide explicit hint concering uniqueness of derivation

tuned signature: eliminated pointless type Context.pretty;

tuned signature;
clarified context;

clarified context;

clarified context;

discontinued pointless warnings: commands are only defined inside a theory context;

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

more uniform "verbose" option to print name space;

proper local Proof_Context.arity_sorts;

clarified context;

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

tuned signature -- prefer qualified names;

modernized and more uniform style

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

eliminated unused int_only flag (see also c12484a27367);
just proper commands;

tracing facilities for the code generator preprocessor

tuned interface

clarified stylized status of sandwich algebra

--HG--
extra : rebase_source : 95023f17add42eb344e0a81a0dbeec7af5fde126

syntactic means to prevent accidental mixup of static and dynamic context

--HG--
extra : rebase_source : 5713560aaa0dd320d68157ba353db0f597594d25

optimization for trivial cases

--HG--
extra : rebase_source : 635e80ef7875b039ddcf0a35f1394b724aaf8528

modernized setup

--HG--
extra : rebase_source : 0cfd0b870c7052c56cc8d7db236a939f1f1f7762

unified approach toward conversions and simple term rewriting in preprocessor by means of sandwiches

--HG--
extra : rebase_source : 7600b4f199b25f6cc02bee69f39743acd6c4e3bb

normalize type variables of evaluation term by conversion

--HG--
extra : rebase_source : 23265651fbca087c1336c0a7feb85f0cbb910e69

delete attribute for code abbrev

normalizing of type variables before evaluation with explicit resubstitution function: make nbe work with funny type variables like \<AA>;
tuned naming;
dropped dead parameters;

some shortcuts for chunks, which sometimes avoid bulky string output;

prefer proof context over background theory

--HG--
extra : rebase_source : 307a2e54d5c0b89d8668ce99110df0538037668e

build up preprocessing context only once

proper context for simplifier invocations in code generation stack

clarified simplifier context;
eliminated Simplifier.global_context;

tuned

--HG--
extra : rebase_source : 6db8e660aefa9aa70ba769e24988d3b9f128cf17

more correct context for dynamic invocations of static code conversions etc.

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

more standard module name Axclass (according to file name);

discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
print timing as tracing, to keep it out of the way in Proof General;
no timing of control commands, especially relevant for Proof General;

close code theorems explicitly after preprocessing

apply preprocessing simpset also to rhs of abstract code equations

maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
more explicit Context.generic for Name_Space.declare/define and derivatives (NB: naming changed after Proof_Context.init_global);
prefer Context.pretty in low-level operations of structure Sorts/Type (defer full Syntax.init_pretty until error output);
simplified signatures;

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

renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;

semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat

--HG--
extra : rebase_source : 7ed52e71daa69142f147737027b94acaef451223

removing redundant attribute code_inline in the code generator

removing declaration of code_unfold to address the old code generator

refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;

code preprocessor applies simplifier when schematic variables are fixed to free variables to allow rewriting with congruence rules in the preprocessing steps

pass plain Proof.context for pretty printing;

simplified pretty printing context, which is only required for certain kernel operations;
disentangled dependencies of structure Pretty;

modernized structure Proof_Context;

canonical handling of theory context argument

clarified exports of structure Simplifier;

more appropriate closures for static evaluation

simplified evaluation function names

tuned

dropped accidental doubled computation

avoid frees and vars in terms to be evaluated by abstracting and applying

separation of static and dynamic thy context

ignore code cache optionally; corrected scope of term value in static_eval_conv

pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;

repaired attribute code_unfold_post which has ever been broken

dropped pre_post_conv

added static_eval_conv

refined and unified naming convention for dynamic code evaluation techniques

minimize sorts in certificate instantiation

tuned titles

added code_simp infrastructure

more consistent naming aroud type classes and instances

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

renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;

of_sort_derivation: pass-through full type information -- following the version by krauss/schropp;

modernized structure Local_Defs;

renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;

simplified

explicit abstract type of code certificates

function transformer preprocessor applies to both code generators

code certificates as integral part of code generation

code cache only persists on equal theories

code cache without copy; tuned

reduced code generator cache to the baremost minimum

tuned

permissive AList.merge -- most likely setup for theory data (beware of spurious AList.DUP);

adapted Theory_Data;
tuned;

map_range (and map_index) combinator

tuned handling of type variable names further

variables in type schemes must be renamed simultaneously with variables in equations

Sorts.of_sort_derivation: no pp here;

moved eq handling in nbe into separate oracle

moved all technical processing of code equations to code_thingol.ML

attempt to move desymbolization to translation

added a somehow clueless comment

cleaned up variable desymbolification and argument expansion

integrated add_triv_classes into evaluation stack

proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;

added code_unfold_post attribute

code attributes use common underscore convention

renamed structure TermSubst to Term_Subst;

renamed functor TableFun to Table, and GraphFun to Graph;

tuned structure Code internally

tuned interface of structure Code

uniformly capitialized names for subdirectories

--HG--
rename : src/HOL/Tools/datatype_package/datatype.ML => src/HOL/Tools/Datatype/datatype.ML
rename : src/HOL/Tools/datatype_package/datatype_abs_proofs.ML => src/HOL/Tools/Datatype/datatype_abs_proofs.ML
rename : src/HOL/Tools/datatype_package/datatype_aux.ML => src/HOL/Tools/Datatype/datatype_aux.ML
rename : src/HOL/Tools/datatype_package/datatype_case.ML => src/HOL/Tools/Datatype/datatype_case.ML
rename : src/HOL/Tools/datatype_package/datatype_codegen.ML => src/HOL/Tools/Datatype/datatype_codegen.ML
rename : src/HOL/Tools/datatype_package/datatype_prop.ML => src/HOL/Tools/Datatype/datatype_prop.ML
rename : src/HOL/Tools/datatype_package/datatype_realizer.ML => src/HOL/Tools/Datatype/datatype_realizer.ML
rename : src/HOL/Tools/datatype_package/datatype_rep_proofs.ML => src/HOL/Tools/Datatype/datatype_rep_proofs.ML
rename : src/HOL/Tools/function_package/auto_term.ML => src/HOL/Tools/Function/auto_term.ML
rename : src/HOL/Tools/function_package/context_tree.ML => src/HOL/Tools/Function/context_tree.ML
rename : src/HOL/Tools/function_package/decompose.ML => src/HOL/Tools/Function/decompose.ML
rename : src/HOL/Tools/function_package/descent.ML => src/HOL/Tools/Function/descent.ML
rename : src/HOL/Tools/function_package/fundef.ML => src/HOL/Tools/Function/fundef.ML
rename : src/HOL/Tools/function_package/fundef_common.ML => src/HOL/Tools/Function/fundef_common.ML
rename : src/HOL/Tools/function_package/fundef_core.ML => src/HOL/Tools/Function/fundef_core.ML
rename : src/HOL/Tools/function_package/fundef_datatype.ML => src/HOL/Tools/Function/fundef_datatype.ML
rename : src/HOL/Tools/function_package/fundef_lib.ML => src/HOL/Tools/Function/fundef_lib.ML
rename : src/HOL/Tools/function_package/induction_scheme.ML => src/HOL/Tools/Function/induction_scheme.ML
rename : src/HOL/Tools/function_package/inductive_wrap.ML => src/HOL/Tools/Function/inductive_wrap.ML
rename : src/HOL/Tools/function_package/lexicographic_order.ML => src/HOL/Tools/Function/lexicographic_order.ML
rename : src/HOL/Tools/function_package/measure_functions.ML => src/HOL/Tools/Function/measure_functions.ML
rename : src/HOL/Tools/function_package/mutual.ML => src/HOL/Tools/Function/mutual.ML
rename : src/HOL/Tools/function_package/pattern_split.ML => src/HOL/Tools/Function/pattern_split.ML
rename : src/HOL/Tools/function_package/scnp_reconstruct.ML => src/HOL/Tools/Function/scnp_reconstruct.ML
rename : src/HOL/Tools/function_package/scnp_solve.ML => src/HOL/Tools/Function/scnp_solve.ML
rename : src/HOL/Tools/function_package/size.ML => src/HOL/Tools/Function/size.ML
rename : src/HOL/Tools/function_package/sum_tree.ML => src/HOL/Tools/Function/sum_tree.ML
rename : src/HOL/Tools/function_package/termination.ML => src/HOL/Tools/Function/termination.ML
rename : src/Tools/code/code_haskell.ML => src/Tools/Code/code_haskell.ML
rename : src/Tools/code/code_ml.ML => src/Tools/Code/code_ml.ML
rename : src/Tools/code/code_preproc.ML => src/Tools/Code/code_preproc.ML
rename : src/Tools/code/code_printer.ML => src/Tools/Code/code_printer.ML
rename : src/Tools/code/code_target.ML => src/Tools/Code/code_target.ML
rename : src/Tools/code/code_thingol.ML => src/Tools/Code/code_thingol.ML