# HG changeset patch
# User nipkow
# Date 1251479759 -7200
# Node ID 66f1a0dfe7d904e21bcf6bbcb3be8b675bfbb9cc
# Parent  10cd49e0c067a137feeaf6cd658817678ef8fecc
tuned proofs

diff -r 10cd49e0c067 -r 66f1a0dfe7d9 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Aug 28 18:52:41 2009 +0200
+++ b/src/HOL/Finite_Set.thy	Fri Aug 28 19:15:59 2009 +0200
@@ -2966,11 +2966,11 @@
 
 lemma dual_max:
   "ord.max (op \<ge>) = min"
-  by (auto simp add: ord.max_def_raw min_def_raw expand_fun_eq)
+  by (auto simp add: ord.max_def_raw expand_fun_eq)
 
 lemma dual_min:
   "ord.min (op \<ge>) = max"
-  by (auto simp add: ord.min_def_raw max_def_raw expand_fun_eq)
+  by (auto simp add: ord.min_def_raw expand_fun_eq)
 
 lemma strict_below_fold1_iff:
   assumes "finite A" and "A \<noteq> {}"
diff -r 10cd49e0c067 -r 66f1a0dfe7d9 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Fri Aug 28 18:52:41 2009 +0200
+++ b/src/HOL/Int.thy	Fri Aug 28 19:15:59 2009 +0200
@@ -266,7 +266,7 @@
 proof  
   fix k :: int
   show "abs k = sup k (- k)"
-    by (auto simp add: sup_int_def zabs_def max_def less_minus_self_iff [symmetric])
+    by (auto simp add: sup_int_def zabs_def less_minus_self_iff [symmetric])
 qed
 
 lemma zless_imp_add1_zle: "w < z \<Longrightarrow> w + (1\<Colon>int) \<le> z"
@@ -1487,21 +1487,6 @@
        add_special diff_special eq_special less_special le_special
 
 
-lemma min_max_01: "min (0::int) 1 = 0 & min (1::int) 0 = 0 &
-                   max (0::int) 1 = 1 & max (1::int) 0 = 1"
-by(simp add:min_def max_def)
-
-lemmas min_max_special[simp] =
- min_max_01
- max_def[of "0::int" "number_of v", standard, simp]
- min_def[of "0::int" "number_of v", standard, simp]
- max_def[of "number_of u" "0::int", standard, simp]
- min_def[of "number_of u" "0::int", standard, simp]
- max_def[of "1::int" "number_of v", standard, simp]
- min_def[of "1::int" "number_of v", standard, simp]
- max_def[of "number_of u" "1::int", standard, simp]
- min_def[of "number_of u" "1::int", standard, simp]
-
 text {* Legacy theorems *}
 
 lemmas zle_int = of_nat_le_iff [where 'a=int]
diff -r 10cd49e0c067 -r 66f1a0dfe7d9 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Fri Aug 28 18:52:41 2009 +0200
+++ b/src/HOL/Nat.thy	Fri Aug 28 19:15:59 2009 +0200
@@ -1512,7 +1512,7 @@
 by (simp split add: nat_diff_split)
 
 lemma min_diff: "min (m - (i::nat)) (n - i) = min m n - i"
-unfolding min_def by auto
+by auto
 
 lemma inj_on_diff_nat: 
   assumes k_le_n: "\<forall>n \<in> N. k \<le> (n::nat)"
diff -r 10cd49e0c067 -r 66f1a0dfe7d9 src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Fri Aug 28 18:52:41 2009 +0200
+++ b/src/HOL/OrderedGroup.thy	Fri Aug 28 19:15:59 2009 +0200
@@ -1275,7 +1275,7 @@
 proof -
   note add_le_cancel_right [of a a "- a", symmetric, simplified]
   moreover note add_le_cancel_right [of "-a" a a, symmetric, simplified]
-  then show ?thesis by (auto simp: sup_max max_def)
+  then show ?thesis by (auto simp: sup_max)
 qed
 
 lemma abs_if_lattice: