--- a/src/HOL/Analysis/Analysis.thy Mon Dec 02 14:22:28 2019 +0100
+++ b/src/HOL/Analysis/Analysis.thy Mon Dec 02 18:29:22 2019 +0100
@@ -12,18 +12,22 @@
Norm_Arith
(* Vector Analysis *)
Convex_Euclidean_Space
+ Operator_Norm
+ (* Unsorted *)
+ Line_Segment
+ Derivative
+ Cartesian_Euclidean_Space
+ Weierstrass_Theorems
(* Measure and Integration Theory *)
Ball_Volume
Integral_Test
Improper_Integral
Equivalence_Measurable_On_Borel
- (* Unsorted *)
Lebesgue_Integral_Substitution
Embed_Measure
Complete_Measure
Radon_Nikodym
Fashoda_Theorem
- Determinants
Cross3
Homeomorphism
Bounded_Continuous_Function
@@ -32,7 +36,6 @@
Lindelof_Spaces
Infinite_Products
Infinite_Set_Sum
- Weierstrass_Theorems
Polytope
Jordan_Curve
Poly_Roots