changeset 66453 | cc19f7ca2ed6 |
parent 66289 | 2562f151541c |
child 66641 | ff2e0115fea4 |
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Fri Aug 18 13:55:05 2017 +0200 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Fri Aug 18 20:47:47 2017 +0200 @@ -11,7 +11,7 @@ theory Convex_Euclidean_Space imports Topology_Euclidean_Space - "~~/src/HOL/Library/Set_Algebras" + "HOL-Library.Set_Algebras" begin lemma swap_continuous: (*move to Topological_Spaces?*)