changeset 68188 | 2af1f142f855 |
parent 68120 | 2f161c6910f7 |
child 68532 | f8b98d31ad45 |
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Tue May 15 06:23:12 2018 +0200 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Tue May 15 11:33:43 2018 +0200 @@ -10,6 +10,7 @@ imports "HOL-Library.Indicator_Function" "HOL-Library.Countable_Set" + "HOL-Library.FuncSet" Linear_Algebra Norm_Arith begin