# HG changeset patch # User haftmann # Date 1266850398 -3600 # Node ID 4bc6b4d70e0893ad4262d61589036e418a7e3093 # Parent 90e42f9ba4d104f709100398a5c7156947a4bb22 tuned text diff -r 90e42f9ba4d1 -r 4bc6b4d70e08 src/HOL/Rings.thy --- a/src/HOL/Rings.thy Mon Feb 22 15:53:18 2010 +0100 +++ b/src/HOL/Rings.thy Mon Feb 22 15:53:18 2010 +0100 @@ -13,19 +13,6 @@ imports Groups begin -text {* - The theory of partially ordered rings is taken from the books: - \begin{itemize} - \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979 - \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963 - \end{itemize} - Most of the used notions can also be looked up in - \begin{itemize} - \item \url{http://www.mathworld.com} by Eric Weisstein et. al. - \item \emph{Algebra I} by van der Waerden, Springer. - \end{itemize} -*} - class semiring = ab_semigroup_add + semigroup_mult + assumes left_distrib[algebra_simps]: "(a + b) * c = a * c + b * c" assumes right_distrib[algebra_simps]: "a * (b + c) = a * b + a * c" @@ -506,6 +493,19 @@ assumes mult_left_mono: "a \ b \ 0 \ c \ c * a \ c * b" assumes mult_right_mono: "a \ b \ 0 \ c \ a * c \ b * c" +text {* + The theory of partially ordered rings is taken from the books: + \begin{itemize} + \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979 + \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963 + \end{itemize} + Most of the used notions can also be looked up in + \begin{itemize} + \item \url{http://www.mathworld.com} by Eric Weisstein et. al. + \item \emph{Algebra I} by van der Waerden, Springer. + \end{itemize} +*} + class ordered_semiring = mult_mono + semiring_0 + ordered_ab_semigroup_add begin