# HG changeset patch
# User nipkow
# Date 1575307762 -3600
# Node ID 26b35a97bddb902bb06cdebb75705eda32cf2569
# Parent  777d673fa672f57ce2b852d32a22886f59c78ac6
tuned manual

diff -r 777d673fa672 -r 26b35a97bddb src/HOL/Analysis/Analysis.thy
--- 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