author haftmann Mon Feb 22 15:53:18 2010 +0100 (2010-02-22) changeset 35302 4bc6b4d70e08 parent 35301 90e42f9ba4d1 child 35303 816e48d60b13
tuned text
 src/HOL/Rings.thy file | annotate | diff | revisions
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.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.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