# HG changeset patch
# User wenzelm
# Date 1085167011 -7200
# Node ID fe9504ba63d503930fd64a7312d140718a76ad61
# Parent  b698d0b243dc86d71eb3bd95c595087b750a2215
removed duplicate thms;

diff -r b698d0b243dc -r fe9504ba63d5 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri May 21 21:15:45 2004 +0200
+++ b/src/HOL/List.thy	Fri May 21 21:16:51 2004 +0200
@@ -1543,12 +1543,6 @@
                 nth_Cons'[of _ _ "number_of v",standard]
 
 
-lemma distinct_card: "distinct xs \<Longrightarrow> card (set xs) = size xs"
-  by (induct xs) auto
-
-lemma card_length: "card (set xs) \<le> length xs"
-  by (induct xs) (auto simp add: card_insert_if)
-
 lemma "card (set xs) = size xs \<Longrightarrow> distinct xs"
 proof (induct xs)
   case Nil thus ?case by simp
diff -r b698d0b243dc -r fe9504ba63d5 src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Fri May 21 21:15:45 2004 +0200
+++ b/src/HOL/OrderedGroup.thy	Fri May 21 21:16:51 2004 +0200
@@ -1,9 +1,6 @@
-(*  Title:   HOL/Group.thy
+(*  Title:   HOL/OrderedGroup.thy
     ID:      $Id$
-    Author:  Gertrud Bauer and Markus Wenzel, TU Muenchen
-             Lawrence C Paulson, University of Cambridge
-             Revised and decoupled from Ring_and_Field.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)
 *)
 
@@ -20,7 +17,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}
 *}
@@ -589,7 +586,6 @@
     hence "0 <= a" by (blast intro: order_trans meet_join_le)
   }
   note p = this
-  thm p
   assume hyp:"join a (-a) = 0"
   hence hyp2:"join (-a) (-(-a)) = 0" by (simp add: join_comm)
   from p[OF hyp] p[OF hyp2] show "a = 0" by simp
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]: