
diff -r 0aaf16a0f7cc -r 3548d54ce3ee src/HOL/Analysis/Analysis.thy
--- a/src/HOL/Analysis/Analysis.thy	Mon Dec 02 14:07:42 2019 -0500
+++ b/src/HOL/Analysis/Analysis.thy	Mon Dec 02 22:40:16 2019 -0500
@@ -46,6 +46,7 @@
   FPS_Convergence
   Smooth_Paths
   Abstract_Euclidean_Space
+  Function_Metric
 begin
 
 end




