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
```