merged

example for executable choice

added simple theory about discrete summation

giving up sunbroy2;

merged

a draft for an example how to turn specifications involving choice executable

added lemma map_of_map_restrict; generalized lemma dom_const

adjusted to changes in theory Mapping

more close integration with theory Map

mappings implemented by association lists

merged

updated SMT certificates

include solver arguments as comments in SMT problem files (to distinguish different results from the same problem when caching results)

updated SMT certificates

added Cache_IO: cache for output of external tools, changed SMT solver interface to use Cache_IO

Rename transp to transpose in HOL-Multivariate_Analysis. (by himmelma)

simplified/clarified record print translations;

eliminated camel case;

tuned;

simplified/clarified record translations;

moved generic update_name to Pure syntax -- not specific to HOL/record;

tuned;

comment;

conceal internal record definitions;

simplified meaning of ProofContext.verbose; eliminated strange ProofContext.setmp_verbose_CRITICAL; less confusing printing of (cumulative) unnamed facts;

refrain from using @{const_name} in syntax translations;

misc tuning and simplification;

refined and exported record_info;

modernized structures;

modernized signature -- proper binding; misc tuning;

tuned errors; tuned;

Typedef.the_info;

formal markup of constants; misc tuning;

tuned document;

eliminated old fold;

renamed InfixName to Infix etc.;

discontinued unnamed infix syntax;

eliminated unnamed infixes;

apply global morphism for theory, instantiation and overloading target; n.b. target morphism and global morphism coincide for theory target

clarifed type

optionally localize assertion labels (based on user-defined offsets) to reduce the effort of label adaptions after changes to the source program

formal markup of constants;

modernized structures;

authentic proof syntax;

tuned import order

tuned comments

merged

merged