src/HOL/Analysis/Path_Connected.thy
changeset 66939 04678058308f
parent 66884 c2128ab11f61
child 66955 289f390c4e57
     1.1 --- a/src/HOL/Analysis/Path_Connected.thy	Sun Oct 29 19:39:03 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Path_Connected.thy	Mon Oct 30 16:02:59 2017 +0000
     1.3 @@ -6969,7 +6969,7 @@
     1.4    shows "S homotopy_eqv ({}::'b::real_normed_vector set) \<longleftrightarrow> S = {}"
     1.5  apply (rule iffI)
     1.6  using homotopy_eqv_def apply fastforce
     1.7 -by (simp add: homotopy_eqv_contractible_sets contractible_empty)
     1.8 +by (simp add: homotopy_eqv_contractible_sets)
     1.9  
    1.10  lemma homotopy_eqv_empty2 [simp]:
    1.11    fixes S :: "'a::real_normed_vector set"