Changes

Summary

1. merged
2. clarified export of consts: recursion is accessible via spec_rules;
3. more operations;
4. Removed orphaned theory from HOL-Analysis
5. merged
6. clarified position for spec rule: like entity;
7. clarified name: avoid clashes;
8. proper dynamic position of application context, e.g. relevant for 'global_interpretation';
9. proper treatment of variable names;
10. proper spec_rule name via naming/binding/Morphism.binding;
11. more informative spec rules;
12. more robust;
13. more informative export;
14. tuned signature -- following Export_Theory.Spec_Rule in Scala;
15. tuned comment;
16. clarified export of spec rules: more like locale;
17. formal position for spec rule (not significant for equality);
18. proper spec rules via resulting def_thm, e.g. relevant for "isabelle build -o export_theory";
19. proper spec rules via fun_lhs, e.g. relevant for "isabelle build -o export_theory";
20. tuned -- avoid confusion of fun_t with fun_lhs;
21. avoid shadowing of local bindings -- more maintainable;
22. export spec rules;
23. Reorganised HOL-Complex_Analysis
24. split off metric spaces part of Function_Topology: subsequent theories Product_Topology, T1_Spaces, Lindelof_Spaces are purely topological