src/HOL/Ring_and_Field.thy
changeset 24515 d4dc5dc2db98
parent 24506 020db6ec334a
child 24748 ee0a0eb6b738
     1.1 --- a/src/HOL/Ring_and_Field.thy	Sat Sep 01 18:17:36 2007 +0200
     1.2 +++ b/src/HOL/Ring_and_Field.thy	Sat Sep 01 18:17:38 2007 +0200
     1.3 @@ -347,8 +347,10 @@
     1.4  
     1.5  class ordered_field = field + ordered_idom
     1.6  
     1.7 -lemmas linorder_neqE_ordered_idom =
     1.8 - linorder_neqE[where 'a = "?'b::ordered_idom"]
     1.9 +lemma linorder_neqE_ordered_idom:
    1.10 +  fixes x y :: "'a :: ordered_idom"
    1.11 +  assumes "x \<noteq> y" obtains "x < y" | "y < x"
    1.12 +  using assms by (rule linorder_neqE)
    1.13  
    1.14  lemma eq_add_iff1:
    1.15    "(a*e + c = b*e + d) = ((a-b)*e + c = (d::'a::ring))"