--- a/src/HOL/Library/Multiset.thy Fri Aug 28 19:15:59 2009 +0200
+++ b/src/HOL/Library/Multiset.thy Fri Aug 28 19:35:49 2009 +0200
@@ -331,7 +331,7 @@
lemma multiset_inter_count:
"count (A #\<inter> B) x = min (count A x) (count B x)"
-by (simp add: multiset_inter_def min_def)
+by (simp add: multiset_inter_def)
lemma multiset_inter_commute: "A #\<inter> B = B #\<inter> A"
by (simp add: multiset_eq_conv_count_eq multiset_inter_count
@@ -353,7 +353,7 @@
by (simp add: multiset_eq_conv_count_eq multiset_inter_count)
lemma multiset_union_diff_commute: "B #\<inter> C = {#} \<Longrightarrow> A + B - C = A - C + B"
-apply (simp add: multiset_eq_conv_count_eq multiset_inter_count min_def
+apply (simp add: multiset_eq_conv_count_eq multiset_inter_count
split: split_if_asm)
apply clarsimp
apply (erule_tac x = a in allE)
--- a/src/HOL/Library/Word.thy Fri Aug 28 19:15:59 2009 +0200
+++ b/src/HOL/Library/Word.thy Fri Aug 28 19:35:49 2009 +0200
@@ -1519,9 +1519,7 @@
proof -
have "((2::int) ^ (length w1 - 1)) + (2 ^ (length w2 - 1)) \<le>
2 ^ (max (length w1) (length w2) - 1) + 2 ^ (max (length w1) (length w2) - 1)"
- apply (cases "length w1 \<le> length w2")
- apply (auto simp add: max_def)
- done
+ by (auto simp:max_def)
also have "... = 2 ^ max (length w1) (length w2)"
proof -
from lw
@@ -2173,16 +2171,16 @@
apply (subst bv_sliceI [where ?j = i and ?i = j and ?w = w and ?w1.0 = "w1 @ w2" and ?w2.0 = w3 and ?w3.0 = "w4 @ w5"])
apply simp_all
apply (rule w_def)
- apply (simp add: w_defs min_def)
- apply (simp add: w_defs min_def)
+ apply (simp add: w_defs)
+ apply (simp add: w_defs)
apply (subst bv_sliceI [where ?j = k and ?i = l and ?w = w and ?w1.0 = w1 and ?w2.0 = "w2 @ w3 @ w4" and ?w3.0 = w5])
apply simp_all
apply (rule w_def)
- apply (simp add: w_defs min_def)
- apply (simp add: w_defs min_def)
+ apply (simp add: w_defs)
+ apply (simp add: w_defs)
apply (subst bv_sliceI [where ?j = "i-k" and ?i = "j-k" and ?w = "w2 @ w3 @ w4" and ?w1.0 = w2 and ?w2.0 = w3 and ?w3.0 = w4])
apply simp_all
- apply (simp_all add: w_defs min_def)
+ apply (simp_all add: w_defs)
done
qed