isabelle update -u control_cartouches;

prefer control symbol antiquotations;

optional timing for code generator conversions

tuned

explicit quasi-global context for nbe conversions -- works around quasi-global type variable handling in lift_triv_classes_conv

clarified naming conventions and code for code evaluation sandwiches

clarified names of variants

Type_Infer.object_logic controls improvement of type inference result;

explicit record values for dictionary variables

moved remaining display.ML to more_thm.ML;

trim context for persistent storage;

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

clarified context;

clarified context;

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

clarified signature;

tuned signature -- prefer qualified names;

tuned;

proper exception for internal program failure, not user-error;

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

tuned data structure

--HG--
extra : rebase_source : 7cc408d038ae0cb3e103cd433b0b20a81851b688

modernized diagnostic options

--HG--
extra : rebase_source : 7c269611b368864afe343dd784ff59d0615fd858

be more explicit: made sml/nj happy

accurate separation of static and dynamic context

--HG--
extra : rebase_source : c4ec1445bba8cce426e6a04157de8511b796ee2d

syntactic means to prevent accidental mixup of static and dynamic context

--HG--
extra : rebase_source : 5713560aaa0dd320d68157ba353db0f597594d25

proper separation of static and dynamic context

--HG--
extra : rebase_source : 1f6a00548956a1575e31153103b3e2a7d2f3ba50

dropped obsolete hand-waving adjustion of type variables: safely done in preprocessor

--HG--
extra : rebase_source : 9e5c02ee3f9e1ecf4b01a5b399ce2acc72f323e2

degeneralized value command into HOL

--HG--
rename : src/Tools/value.ML => src/HOL/Tools/value.ML

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

more qualified names;

prefer proof context over background theory

--HG--
extra : rebase_source : 307a2e54d5c0b89d8668ce99110df0538037668e

made smlnj happy

less clumsy namespace

prefer explicit code symbol type over ad-hoc name mangling

prefer indexes user for pattern matching to print concrete names for symbols, do not rely on printable unique identifiers

explicit distinction between empty code equations and no code equations, including convenient declaration attributes

explicit hint for domain of class parameters in instance statements

formally accept dictionary parameters for constants on left hand sides in equations

--HG--
extra : rebase_source : 1f057e1453fc022600a1a01769a4b0d6a735e17a

do not choke on type variables emerging during rewriting

--HG--
extra : rebase_source : 67c2b69336b1234e9ec1dd86ae5ea80e51f082e6

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

prefer records with speaking labels over deeply nested tuples

--HG--
extra : rebase_source : 09acb7079a2d06a9c7f68aaaf04cedb0752142e0

dropped dead code

corrected Nbe.static_value: ignore cached compilations;
tuned

tuned heading

--HG--
extra : rebase_source : 24638b19082d4215acbd7495e0a8b83f0dced3b0

adding the body type as well to the code generation for constants as it is required for type annotations of constants

changing const type to pass along if typing annotations are necessary for disambigous terms

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

proper @{binding} antiquotations (relevant for formal references);

tuned signature: Name.invent and Name.invent_names;

prefer new-style Name.invents;

split Type_Infer into early and late part, after Proof_Context;
added Type_Infer_Context.const_sorts option, which allows NBE to use regular Syntax.check_term;

modernized structure Proof_Context;

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

canonical handling of theory context argument

avoid slightly odd Conv.tap_thy

simplified evaluation function names

separated dictionary weakning into separate type

dictionary constants must permit explicit weakening of classes;
tuned names

tuned whitespace

removed experimental equality checking of closures; acknowledge underapproximation of equality in function name

nbe decides equality of abstractions by extensionality

added forall2 predicate lifter

Code.check_const etc.: reject too specific types

moved ML_Context.value to Code_Runtime

no_frees_* is subsumed by new framework mechanisms in Code_Preproc

separation of static and dynamic thy context

tuned whitespace

static nbe conversion

dropped redundant normal_form command

more clear separation of static compilation and dynamic evaluation

replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references

load type_infer.ML later -- proper context for Type_Infer.infer_types;
renamed Type_Infer.polymorphicT to Type.mark_polymorphic;

eliminated aliases of Type.constraint;

turned show_sorts/show_types into proper configuration options;

evaluate takes ml context and ml expression parameter

tuned

use conv alias

refined and unified naming convention for dynamic code evaluation techniques

more precise code

transitive superclasses were also only a misunderstanding

formal introduction of transitive superclasses

dropped obscure type argument weakening mapping -- was only a misunderstanding

added code_simp infrastructure

formal introduction of case cong

more consistent naming aroud type classes and instances

renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;

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

new version of triv_of_class machinery without legacy_unconstrain

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

reactivated Thm.legacy_unconstrainT for Nbe.lift_triv_classes_conv;

just one version of Thm.unconstrainT, which affects all variables;
temporary workaround for Nbe.lift_triv_classes_conv;

renamed Thm.freezeT to Thm.legacy_freezeT -- it is based on Type.legacy_freeze;

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

renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;

dropped superfluous naming

tuned whitespace

code cache only persists on equal theories

code cache without copy; tuned

reduced code generator cache to the baremost minimum

adapted Theory_Data;
tuned;

uniform use of Integer.add/mult/sum/prod;

indicate CRITICAL nature of various setmp combinators;

explicit indication of Unsynchronized.ref;

moved eq handling in nbe into separate oracle

integrated add_triv_classes into evaluation stack

tuned structure Code internally

tuned interface of structure Code

all variable names are optional

variable names in abstractions are optional

more appropriate syntax for IML abstraction

merged module code_unit.ML into code.ML

treat frees driectly by the LCF kernel

explicit type arguments in constants

generic postprocessing scheme for term evaluations

re-engineering of evaluation conversions

diagnostic commands now in code_thingol; tuned code of funny continuations

more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;

Thm.add_oracle interface: replaced old bstring by binding;

Merge.

maintain order of constructors in datatypes; clarified conventions for type schemes

use regular Term.add_XXX etc.;

restored incremental code generation

code identifier namings are no longer imperative

clarified codegen interfaces

non left-linear equations for nbe

case default fallback for NBE

made SMLNJ happy

simplified oracle interface;

ML_Context.evaluate: proper context (for ML environment);

generic value command

restructured and split code serializer module

tuned code theorem bookkeeping

clarified code

simplified TypeInfer.infer_types;

major refactorings in code generator modules

explicit type schemes for functions

command 'normal_form': proper context via Variable.auto_fixes;

cat_lines;

moved 'trivial classes' to foundation of code generator

different handling of eq class for nbe

using integers for pattern matching

cleaned up evaluation interfaces

tuned

tuned

improved implementation

tuned comment

replaced Secure.evaluate by ML_Context.evaluate;

clarified implementation

fixed typo

now employing dictionaries

tuned CRITICAL markups;

evaluation is CRITICAL

generic Syntax.pretty/string_of operations;

simplified interfaces for outer syntax;

step towards proper purge operation

tuned functor application;

TypeInfer.constrain: canonical argument order;

simplified PrintMode interfaces;

avoid direct access to print_mode;

delayed evaluation

replaced ProofContext.read_term/prop by general Syntax.read_term/prop;

replaced ProofContext.infer_types by general Syntax.check_terms;

overloaded definitions accompanied by explicit constants

improved evaluation interface

explizit dependencies

added evaluation examples

tuned

new structure for code generator modules

new nbe implementation

nbe improved