src/HOL/Word/WordShift.thy

--- a/src/HOL/Word/WordShift.thy	Fri Aug 28 19:35:49 2009 +0200
+++ b/src/HOL/Word/WordShift.thy	Fri Aug 28 19:43:19 2009 +0200
@@ -319,7 +319,7 @@
 
 lemma bl_shiftl:
   "to_bl (w << n) = drop n (to_bl w) @ replicate (min (size w) n) False"
-  by (simp add: shiftl_bl word_rep_drop word_size min_def)
+  by (simp add: shiftl_bl word_rep_drop word_size)
 
 lemma shiftl_zero_size: 
   fixes x :: "'a::len0 word"
@@ -1018,8 +1018,7 @@
   word_of_int (bin_cat w (size b) (uint b))"
   apply (unfold word_cat_def word_size) 
   apply (clarsimp simp add : word_ubin.norm_eq_iff [symmetric]
-      word_ubin.eq_norm bintr_cat min_def)
-  apply arith
+      word_ubin.eq_norm bintr_cat)
   done
 
 lemma word_cat_split_alt: