--- 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
--- 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
--- 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]: