# HG changeset patch
# User haftmann
# Date 1265634414 -3600
# Node ID 748f0bc3f7caa071f55cb148ea8d55e7fe8be168
# Parent  b8c8d01cc20d4bd4eb497854f488dbf17ec19900
moved auxiliary lemmas to more appropriate places

diff -r b8c8d01cc20d -r 748f0bc3f7ca src/HOL/SupInf.thy
--- a/src/HOL/SupInf.thy	Mon Feb 08 14:06:51 2010 +0100
+++ b/src/HOL/SupInf.thy	Mon Feb 08 14:06:54 2010 +0100
@@ -6,38 +6,6 @@
 imports RComplete
 begin
 
-lemma minus_max_eq_min:
-  fixes x :: "'a::{lattice_ab_group_add, linorder}"
-  shows "- (max x y) = min (-x) (-y)"
-by (metis le_imp_neg_le linorder_linear min_max.inf_absorb2 min_max.le_iff_inf min_max.le_iff_sup min_max.sup_absorb1)
-
-lemma minus_min_eq_max:
-  fixes x :: "'a::{lattice_ab_group_add, linorder}"
-  shows "- (min x y) = max (-x) (-y)"
-by (metis minus_max_eq_min minus_minus)
-
-lemma minus_Max_eq_Min [simp]:
-  fixes S :: "'a::{lattice_ab_group_add, linorder} set"
-  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Max S) = Min (uminus ` S)"
-proof (induct S rule: finite_ne_induct)
-  case (singleton x)
-  thus ?case by simp
-next
-  case (insert x S)
-  thus ?case by (simp add: minus_max_eq_min) 
-qed
-
-lemma minus_Min_eq_Max [simp]:
-  fixes S :: "'a::{lattice_ab_group_add, linorder} set"
-  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Min S) = Max (uminus ` S)"
-proof (induct S rule: finite_ne_induct)
-  case (singleton x)
-  thus ?case by simp
-next
-  case (insert x S)
-  thus ?case by (simp add: minus_min_eq_max) 
-qed
-
 instantiation real :: Sup 
 begin
 definition