src/HOL/Ring_and_Field.thy
changeset 24515 d4dc5dc2db98
parent 24506 020db6ec334a
child 24748 ee0a0eb6b738
equal deleted inserted replaced
24514:540eaf87e42d 24515:d4dc5dc2db98
   345 
   345 
   346 instance ordered_idom \<subseteq> pordered_comm_ring ..
   346 instance ordered_idom \<subseteq> pordered_comm_ring ..
   347 
   347 
   348 class ordered_field = field + ordered_idom
   348 class ordered_field = field + ordered_idom
   349 
   349 
   350 lemmas linorder_neqE_ordered_idom =
   350 lemma linorder_neqE_ordered_idom:
   351  linorder_neqE[where 'a = "?'b::ordered_idom"]
   351   fixes x y :: "'a :: ordered_idom"
       
   352   assumes "x \<noteq> y" obtains "x < y" | "y < x"
       
   353   using assms by (rule linorder_neqE)
   352 
   354 
   353 lemma eq_add_iff1:
   355 lemma eq_add_iff1:
   354   "(a*e + c = b*e + d) = ((a-b)*e + c = (d::'a::ring))"
   356   "(a*e + c = b*e + d) = ((a-b)*e + c = (d::'a::ring))"
   355 by (simp add: ring_simps)
   357 by (simp add: ring_simps)
   356 
   358