src/HOL/Rings.thy
changeset 35302 4bc6b4d70e08
parent 35216 7641e8d831d2
child 35631 0b8a5fd339ab
     1.1 --- a/src/HOL/Rings.thy	Mon Feb 22 15:53:18 2010 +0100
     1.2 +++ b/src/HOL/Rings.thy	Mon Feb 22 15:53:18 2010 +0100
     1.3 @@ -13,19 +13,6 @@
     1.4  imports Groups
     1.5  begin
     1.6  
     1.7 -text {*
     1.8 -  The theory of partially ordered rings is taken from the books:
     1.9 -  \begin{itemize}
    1.10 -  \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979 
    1.11 -  \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
    1.12 -  \end{itemize}
    1.13 -  Most of the used notions can also be looked up in 
    1.14 -  \begin{itemize}
    1.15 -  \item \url{http://www.mathworld.com} by Eric Weisstein et. al.
    1.16 -  \item \emph{Algebra I} by van der Waerden, Springer.
    1.17 -  \end{itemize}
    1.18 -*}
    1.19 -
    1.20  class semiring = ab_semigroup_add + semigroup_mult +
    1.21    assumes left_distrib[algebra_simps]: "(a + b) * c = a * c + b * c"
    1.22    assumes right_distrib[algebra_simps]: "a * (b + c) = a * b + a * c"
    1.23 @@ -506,6 +493,19 @@
    1.24    assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
    1.25    assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
    1.26  
    1.27 +text {*
    1.28 +  The theory of partially ordered rings is taken from the books:
    1.29 +  \begin{itemize}
    1.30 +  \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979 
    1.31 +  \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
    1.32 +  \end{itemize}
    1.33 +  Most of the used notions can also be looked up in 
    1.34 +  \begin{itemize}
    1.35 +  \item \url{http://www.mathworld.com} by Eric Weisstein et. al.
    1.36 +  \item \emph{Algebra I} by van der Waerden, Springer.
    1.37 +  \end{itemize}
    1.38 +*}
    1.39 +
    1.40  class ordered_semiring = mult_mono + semiring_0 + ordered_ab_semigroup_add 
    1.41  begin
    1.42