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