# HG changeset patch
# User hoelzl
# Date 1362585381 -3600
# Node ID 8ee3778235185e401708b3ba17f80e4f2837f3b5
# Parent  d4d00c804645f41847ecb46cbcb1014dbf8d9950
tuned proofs

diff -r d4d00c804645 -r 8ee377823518 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Mar 06 16:56:21 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Mar 06 16:56:21 2013 +0100
@@ -6315,20 +6315,18 @@
   show ?th unfolding homeomorphic_minimal
     apply(rule_tac x="\<lambda>x. b + (e/d) *\<^sub>R (x - a)" in exI)
     apply(rule_tac x="\<lambda>x. a + (d/e) *\<^sub>R (x - b)" in exI)
-    using assms apply (auto simp add: dist_commute)
-    unfolding dist_norm
-    apply (auto simp add: pos_divide_less_eq mult_strict_left_mono)
-    unfolding continuous_on
-    by (intro ballI tendsto_intros, simp)+
+    using assms
+    apply (auto intro!: continuous_on_intros
+                simp: dist_commute dist_norm pos_divide_less_eq mult_strict_left_mono)
+    done
 next
   show ?cth unfolding homeomorphic_minimal
     apply(rule_tac x="\<lambda>x. b + (e/d) *\<^sub>R (x - a)" in exI)
     apply(rule_tac x="\<lambda>x. a + (d/e) *\<^sub>R (x - b)" in exI)
-    using assms apply (auto simp add: dist_commute)
-    unfolding dist_norm
-    apply (auto simp add: pos_divide_le_eq)
-    unfolding continuous_on
-    by (intro ballI tendsto_intros, simp)+
+    using assms
+    apply (auto intro!: continuous_on_intros
+                simp: dist_commute dist_norm pos_divide_le_eq mult_strict_left_mono)
+    done
 qed
 
 text{* "Isometry" (up to constant bounds) of injective linear map etc.           *}