src/HOL/Analysis/Homotopy.thy
changeset 70033 6cbc7634135c
parent 69986 f2d327275065
child 70136 f03a01a18c6e
     1.1 --- a/src/HOL/Analysis/Homotopy.thy	Tue Apr 02 14:46:01 2019 +0200
     1.2 +++ b/src/HOL/Analysis/Homotopy.thy	Tue Apr 02 14:51:27 2019 +0200
     1.3 @@ -3815,9 +3815,9 @@
     1.4        apply (rule_tac x=a in bexI)
     1.5         apply (rule_tac x=b in bexI)
     1.6        using homotopic_with_prod_topology [OF a b]
     1.7 -    	  apply (metis (no_types, lifting) case_prod_Pair case_prod_beta' eq_id_iff)
     1.8 -    	 apply auto
     1.9 -    	done
    1.10 +        apply (metis (no_types, lifting) case_prod_Pair case_prod_beta' eq_id_iff)
    1.11 +       apply auto
    1.12 +      done
    1.13    qed
    1.14    with False show ?thesis
    1.15      by auto