--- a/src/HOL/Homology/Simplices.thy Mon Dec 02 14:07:42 2019 -0500
+++ b/src/HOL/Homology/Simplices.thy Mon Dec 02 22:40:16 2019 -0500
@@ -1,8 +1,10 @@
section\<open>Homology, I: Simplices\<close>
theory "Simplices"
- imports "HOL-Analysis.Abstract_Euclidean_Space" "HOL-Algebra.Free_Abelian_Groups"
-
+ imports
+ "HOL-Analysis.Function_Metric"
+ "HOL-Analysis.Abstract_Euclidean_Space"
+ "HOL-Algebra.Free_Abelian_Groups"
begin
subsection\<open>Standard simplices, all of which are topological subspaces of @{text"R^n"}. \<close>