src/HOL/Analysis/Analysis.thy

new material connected with HOL Light measure theory, plus more rationalisation

+
−theory Analysis
+
−imports
+
−  Regularity
+
−  Lebesgue_Integral_Substitution
+
−  Embed_Measure
+
−  Complete_Measure
+
−  Radon_Nikodym
+
−  Fashoda_Theorem
+
−  Determinants
+
−  Homeomorphism
+
−  Bounded_Continuous_Function
+
−  Weierstrass_Theorems
+
−  Polytope
+
−  Poly_Roots
+
−  Conformal_Mappings
+
−  Generalised_Binomial_Theorem
+
−  Gamma_Function
+
−begin
+
−
+
−end