Summary
- merged
- tuned;
- 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;