Changes

Summary

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