src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
 changeset 57865 dcfb33c26f50 parent 57514 bdc2c6b40bf2 child 58184 db1381d811ab
```     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Aug 05 16:21:27 2014 +0200
1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Aug 05 16:58:19 2014 +0200
1.3 @@ -7307,27 +7307,27 @@
1.4
1.5  lemma real_affinity_le:
1.6   "0 < (m::'a::linordered_field) \<Longrightarrow> (m * x + c \<le> y \<longleftrightarrow> x \<le> inverse(m) * y + -(c / m))"
1.7 -  by (simp add: field_simps inverse_eq_divide)
1.8 +  by (simp add: field_simps)
1.9
1.10  lemma real_le_affinity:
1.11   "0 < (m::'a::linordered_field) \<Longrightarrow> (y \<le> m * x + c \<longleftrightarrow> inverse(m) * y + -(c / m) \<le> x)"
1.12 -  by (simp add: field_simps inverse_eq_divide)
1.13 +  by (simp add: field_simps)
1.14
1.15  lemma real_affinity_lt:
1.16   "0 < (m::'a::linordered_field) \<Longrightarrow> (m * x + c < y \<longleftrightarrow> x < inverse(m) * y + -(c / m))"
1.17 -  by (simp add: field_simps inverse_eq_divide)
1.18 +  by (simp add: field_simps)
1.19
1.20  lemma real_lt_affinity:
1.21   "0 < (m::'a::linordered_field) \<Longrightarrow> (y < m * x + c \<longleftrightarrow> inverse(m) * y + -(c / m) < x)"
1.22 -  by (simp add: field_simps inverse_eq_divide)
1.23 +  by (simp add: field_simps)
1.24
1.25  lemma real_affinity_eq:
1.26   "(m::'a::linordered_field) \<noteq> 0 \<Longrightarrow> (m * x + c = y \<longleftrightarrow> x = inverse(m) * y + -(c / m))"
1.27 -  by (simp add: field_simps inverse_eq_divide)
1.28 +  by (simp add: field_simps)
1.29
1.30  lemma real_eq_affinity:
1.31   "(m::'a::linordered_field) \<noteq> 0 \<Longrightarrow> (y = m * x + c  \<longleftrightarrow> inverse(m) * y + -(c / m) = x)"
1.32 -  by (simp add: field_simps inverse_eq_divide)
1.33 +  by (simp add: field_simps)
1.34
1.35
1.36  subsection {* Banach fixed point theorem (not really topological...) *}
```