Changes

Summary

1. merged
2. tuned;
3. misc tuning and clarification;
4. tuned;
5. tuned -- allow slightly more expensive atomic proofs;
6. clarified signature -- some operations to support fully explicit proof terms;
7. tuned;
8. tuned;
9. proper treatment of sorts;
10. tuned app_types: more direct map_proof_types_same;
11. tuned;
12. generalized parsing, for e.g. Leo-III
13. More theorems about limits, including cancellation simprules
14. Generalised two results concerning limits from the real numbers to type classes
15. formally augmented corresponding rules for field_simps