changeset 15923 | 01d5d0c1c078 |
parent 15769 | 38c8ea8521e7 |
child 16568 | e02fe7ae212b |
--- a/src/HOL/Ring_and_Field.thy Wed May 04 08:37:45 2005 +0200 +++ b/src/HOL/Ring_and_Field.thy Wed May 04 10:42:43 2005 +0200 @@ -245,6 +245,9 @@ axclass ordered_field \<subseteq> field, ordered_idom +lemmas linorder_neqE_ordered_idom = + linorder_neqE[where 'a = "?'b::ordered_idom"] + lemma eq_add_iff1: "(a*e + c = b*e + d) = ((a-b)*e + c = (d::'a::ring))" apply (simp add: diff_minus left_distrib)