diff -r 66f1a0dfe7d9 -r 620a5d8cfa78 src/HOL/Library/Word.thy --- 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)) \ 2 ^ (max (length w1) (length w2) - 1) + 2 ^ (max (length w1) (length w2) - 1)" - apply (cases "length w1 \ 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