eliminated hard TABs;
authorwenzelm
Tue, 02 Apr 2019 14:51:27 +0200
changeset 70215 6cbc7634135c
parent 70214 0674c24afc5e
child 70216 6f2ab7f150f6
eliminated hard TABs;
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