src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 44516 d9a496ae5d9d
parent 44457 d366fa5551ef
child 44517 68e8eb0ce8aa
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 24 12:39:42 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 24 15:06:13 2011 -0700
     1.3 @@ -7,7 +7,7 @@
     1.4  header {* Elementary topology in Euclidean space. *}
     1.5  
     1.6  theory Topology_Euclidean_Space
     1.7 -imports SEQ Linear_Algebra "~~/src/HOL/Library/Glbs"
     1.8 +imports SEQ Linear_Algebra "~~/src/HOL/Library/Glbs" Norm_Arith
     1.9  begin
    1.10  
    1.11  (* to be moved elsewhere *)
    1.12 @@ -5763,15 +5763,13 @@
    1.13    { fix y assume "m > 0"  "m *\<^sub>R a + c \<le> y"  "y \<le> m *\<^sub>R b + c"
    1.14      hence "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}"
    1.15        unfolding image_iff Bex_def mem_interval eucl_le[where 'a='a]
    1.16 -      apply(auto simp add: pth_3[symmetric] 
    1.17 -        intro!: exI[where x="(1 / m) *\<^sub>R (y - c)"]) 
    1.18 +      apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
    1.19        by(auto simp add: pos_le_divide_eq pos_divide_le_eq mult_commute diff_le_iff)
    1.20    } moreover
    1.21    { fix y assume "m *\<^sub>R b + c \<le> y" "y \<le> m *\<^sub>R a + c" "m < 0"
    1.22      hence "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}"
    1.23        unfolding image_iff Bex_def mem_interval eucl_le[where 'a='a]
    1.24 -      apply(auto simp add: pth_3[symmetric]
    1.25 -        intro!: exI[where x="(1 / m) *\<^sub>R (y - c)"])
    1.26 +      apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
    1.27        by(auto simp add: neg_le_divide_eq neg_divide_le_eq mult_commute diff_le_iff)
    1.28    }
    1.29    ultimately show ?thesis using False by auto