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