#563 (Feb 24, 2018, 12:50:08 AM)

1. merged (detail / hgweb)
2. tuned signature; (detail / hgweb)
3. tuned signature; (detail / hgweb)
4. tuned signature; (detail / hgweb)
5. removed unused clone of (map o apsnd);
   removed unused variant of HOLogic.mk_obj_eq; (detail / hgweb)
6. prefer existing HOLogic.mk_obj_eq, despite subtle semantic differences of COMP vs. RS; (detail / hgweb)
7. added HOLogic.mk_obj_eq convenience and eliminated some clones; (detail / hgweb)
8. tuned -- use existing Morphism.instantiate_morphism; (detail / hgweb)
9. Merged; (detail / hgweb)
10. merged (detail / hgweb)
11. Unified the order of zeros and poles; improved reasoning around non-essential singularites (detail / hgweb)
12. merged (detail / hgweb)
13. tuned; (detail / hgweb)
14. tuned signature -- eliminated clones; (detail / hgweb)
15. command 'interpret' no longer exposes resulting theorems as literal facts; (detail / hgweb)
16. 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)
17. tuned; (detail / hgweb)
18. more standard instantiate operations, where substitutions are already certified and stored with trimmed theory certificate; (detail / hgweb)
19. explicit operations to instantiate frees: typ, term, thm, morphism; (detail / hgweb)
20. more operations for ctyp, cterm; (detail / hgweb)
21. minor tuning and clarification; (detail / hgweb)
22. minor tuning and clarification; (detail / hgweb)
23. tuned signature; (detail / hgweb)
24. fixed the proof of pair_measure_count_space (detail / hgweb)
25. merged (detail / hgweb)
26. fixing ennreal using add_mono1; shifting results from linordered_semidom to linordered_nonzero_semiring (detail / hgweb)
27. merged (detail / hgweb)
28. type class linordered_nonzero_semiring has new axiom to guarantee characteristic 0 (detail / hgweb)
29. simplified Radix_Sort (detail / hgweb)

Started by an SCM change

This run spent:

• 5.8 sec waiting;
• 1 hr 31 min build duration;
• 1 hr 31 min total from scheduled to completion.