src/HOL/Ring_and_Field.thy
changeset 15140 322485b816ac
parent 15131 c69542757a4d
child 15178 5f621aa35c25
equal deleted inserted replaced
15139:58cd3404cf75 15140:322485b816ac
     4 *)
     4 *)
     5 
     5 
     6 header {* (Ordered) Rings and Fields *}
     6 header {* (Ordered) Rings and Fields *}
     7 
     7 
     8 theory Ring_and_Field 
     8 theory Ring_and_Field 
     9 import OrderedGroup
     9 imports OrderedGroup
    10 begin
    10 begin
    11 
    11 
    12 text {*
    12 text {*
    13   The theory of partially ordered rings is taken from the books:
    13   The theory of partially ordered rings is taken from the books:
    14   \begin{itemize}
    14   \begin{itemize}