made internal name generation in case expressions more robust

merged

clarified export of consts: recursion is accessible via spec_rules;

more operations;

Removed orphaned theory from HOL-Analysis

merged

clarified position for spec rule: like entity;

clarified name: avoid clashes;

proper dynamic position of application context, e.g. relevant for 'global_interpretation';

proper treatment of variable names;

proper spec_rule name via naming/binding/Morphism.binding;

more informative spec rules;

more robust;

more informative export;

tuned signature -- following Export_Theory.Spec_Rule in Scala;

tuned comment;

clarified export of spec rules: more like locale;

formal position for spec rule (not significant for equality);

proper spec rules via resulting def_thm, e.g. relevant for "isabelle build -o export_theory";

proper spec rules via fun_lhs, e.g. relevant for "isabelle build -o export_theory";

tuned -- avoid confusion of fun_t with fun_lhs;

avoid shadowing of local bindings -- more maintainable;

export spec rules;

Reorganised HOL-Complex_Analysis

split off metric spaces part of Function_Topology: subsequent theories Product_Topology, T1_Spaces, Lindelof_Spaces are purely topological

merged

tuned Analysis manual

tuned Analysis manual

more rules

tuned material