diff -r b698d0b243dc -r fe9504ba63d5 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Fri May 21 21:15:45 2004 +0200
+++ b/src/HOL/Ring_and_Field.thy	Fri May 21 21:16:51 2004 +0200
@@ -1,9 +1,6 @@
 (*  Title:   HOL/Ring_and_Field.thy
     ID:      $Id$
-    Author:  Gertrud Bauer and Markus Wenzel, TU Muenchen
-             Lawrence C Paulson, University of Cambridge
-             Revised and splitted into Ring_and_Field.thy and Group.thy 
-             by Steven Obua, TU Muenchen, in May 2004
+    Author:  Gertrud Bauer, Steven Obua, Lawrence C Paulson and Markus Wenzel
     License: GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 
@@ -19,7 +16,7 @@
   \end{itemize}
   Most of the used notions can also be looked up in 
   \begin{itemize}
-  \item \emph{www.mathworld.com} by Eric Weisstein et. al.
+  \item \url{http://www.mathworld.com} by Eric Weisstein et. al.
   \item \emph{Algebra I} by van der Waerden, Springer.
   \end{itemize}
 *}
@@ -416,18 +413,6 @@
 
 subsection{*More Monotonicity*}
 
-lemma mult_left_mono_neg:
-     "[|b \<le> a; c \<le> 0|] ==> c * a \<le> c * (b::'a::pordered_ring)"
-apply (drule mult_left_mono [of _ _ "-c"]) 
-apply (simp_all add: minus_mult_left [symmetric]) 
-done
-
-lemma mult_right_mono_neg:
-     "[|b \<le> a; c \<le> 0|] ==> a * c \<le> b * (c::'a::pordered_ring)"
-apply (drule mult_right_mono [of _ _ "-c"]) 
-apply (simp_all add: minus_mult_right [symmetric]) 
-done  
-
 text{*Strict monotonicity in both arguments*}
 lemma mult_strict_mono:
      "[|a<b; c<d; 0<b; 0\<le>c|] ==> a * c < b * (d::'a::ordered_semiring_strict)"
@@ -543,7 +528,7 @@
   add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2
   diff_eq_eq eq_diff_eq
     
-thm ring_eq_simps
+
 subsection {* Fields *}
 
 lemma right_inverse [simp]: