#1481 (Feb 23, 2018, 4:55:06 PM)

1. merged (detail / hgweb)
2. tuned; (detail / hgweb)
3. tuned signature -- eliminated clones; (detail / hgweb)
4. command 'interpret' no longer exposes resulting theorems as literal facts; (detail / hgweb)
5. 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; (detail / hgweb)
6. tuned; (detail / hgweb)
7. more standard instantiate operations, where substitutions are already certified and stored with trimmed theory certificate; (detail / hgweb)
8. explicit operations to instantiate frees: typ, term, thm, morphism; (detail / hgweb)
9. more operations for ctyp, cterm; (detail / hgweb)
10. minor tuning and clarification; (detail / hgweb)
11. minor tuning and clarification; (detail / hgweb)
12. tuned signature; (detail / hgweb)

Started by an SCM change

This run spent:

• 5 min 3 sec waiting;
• 2 hr 16 min build duration;
• 2 hr 21 min total from scheduled to completion.