Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 35028 108662d50512
parent 34999 5312d2ffee3b
child 35172 579dd5570f96 
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Feb 05 14:33:31 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Feb 05 14:33:50 2010 +0100
@@ -5696,27 +5696,27 @@
 by (simp add: vector_smult_lneg[symmetric] vector_smult_assoc vector_sneg_minus1[symmetric])
 
 lemma real_affinity_le:
- "0 < (m::'a::ordered_field) ==> (m * x + c \<le> y \<longleftrightarrow> x \<le> inverse(m) * y + -(c / m))"
+ "0 < (m::'a::linordered_field) ==> (m * x + c \<le> y \<longleftrightarrow> x \<le> inverse(m) * y + -(c / m))"
   by (simp add: field_simps inverse_eq_divide)
 
 lemma real_le_affinity:
- "0 < (m::'a::ordered_field) ==> (y \<le> m * x + c \<longleftrightarrow> inverse(m) * y + -(c / m) \<le> x)"
+ "0 < (m::'a::linordered_field) ==> (y \<le> m * x + c \<longleftrightarrow> inverse(m) * y + -(c / m) \<le> x)"
   by (simp add: field_simps inverse_eq_divide)
 
 lemma real_affinity_lt:
- "0 < (m::'a::ordered_field) ==> (m * x + c < y \<longleftrightarrow> x < inverse(m) * y + -(c / m))"
+ "0 < (m::'a::linordered_field) ==> (m * x + c < y \<longleftrightarrow> x < inverse(m) * y + -(c / m))"
   by (simp add: field_simps inverse_eq_divide)
 
 lemma real_lt_affinity:
- "0 < (m::'a::ordered_field) ==> (y < m * x + c \<longleftrightarrow> inverse(m) * y + -(c / m) < x)"
+ "0 < (m::'a::linordered_field) ==> (y < m * x + c \<longleftrightarrow> inverse(m) * y + -(c / m) < x)"
   by (simp add: field_simps inverse_eq_divide)
 
 lemma real_affinity_eq:
- "(m::'a::ordered_field) \<noteq> 0 ==> (m * x + c = y \<longleftrightarrow> x = inverse(m) * y + -(c / m))"
+ "(m::'a::linordered_field) \<noteq> 0 ==> (m * x + c = y \<longleftrightarrow> x = inverse(m) * y + -(c / m))"
   by (simp add: field_simps inverse_eq_divide)
 
 lemma real_eq_affinity:
- "(m::'a::ordered_field) \<noteq> 0 ==> (y = m * x + c  \<longleftrightarrow> inverse(m) * y + -(c / m) = x)"
+ "(m::'a::linordered_field) \<noteq> 0 ==> (y = m * x + c  \<longleftrightarrow> inverse(m) * y + -(c / m) = x)"
   by (simp add: field_simps inverse_eq_divide)
 
 lemma vector_affinity_eq:
isabelle