# HG changeset patch
# User wenzelm
# Date 1554209487 -7200
# Node ID 6cbc7634135c9a2572b83d4f4b2084b030ae724b
# Parent  0674c24afc5e7b07ca5a572a4d19011c9bf40355
eliminated hard TABs;

diff -r 0674c24afc5e -r 6cbc7634135c src/HOL/Analysis/Homotopy.thy
--- a/src/HOL/Analysis/Homotopy.thy	Tue Apr 02 14:46:01 2019 +0200
+++ b/src/HOL/Analysis/Homotopy.thy	Tue Apr 02 14:51:27 2019 +0200
@@ -3815,9 +3815,9 @@
       apply (rule_tac x=a in bexI)
        apply (rule_tac x=b in bexI)
       using homotopic_with_prod_topology [OF a b]
-    	  apply (metis (no_types, lifting) case_prod_Pair case_prod_beta' eq_id_iff)
-    	 apply auto
-    	done
+        apply (metis (no_types, lifting) case_prod_Pair case_prod_beta' eq_id_iff)
+       apply auto
+      done
   qed
   with False show ?thesis
     by auto