tuned signature -- eliminated clones;

command 'interpret' no longer exposes resulting theorems as literal facts;

more robust normalization of witness, e.g. relevant for proofs of transfer_existence_ivl0, transfer_flow0 in AFP/thys/Ordinary_Differential_Equations/Numerics/Transfer_Euclidean_Space_Vector.thy;

tuned;

more standard instantiate operations, where substitutions are already certified and stored with trimmed theory certificate;

explicit operations to instantiate frees: typ, term, thm, morphism;

more operations for ctyp, cterm;

minor tuning and clarification;

minor tuning and clarification;

tuned signature;

fixed the proof of pair_measure_count_space

merged

fixing ennreal using add_mono1; shifting results from linordered_semidom to linordered_nonzero_semiring

merged

type class linordered_nonzero_semiring has new axiom to guarantee characteristic 0

simplified Radix_Sort

merged

merged

moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations

simplified def of stable

Lots of new material about matrices, etc.

tuned proofs -- prefer explicit names for facts from 'interpret';

merged

eliminated questionable Par_List.map -- locale interpretation is mostly lazy (see also b81f1de9f57e);

tuned signature;

tuned;

use lazy notes for locale context init and later additions of facts;

avoid premature Lazy.force due to strict "?" operator;