--- 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> {}"
--- 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]
--- 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)"
--- 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: