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




