# HG changeset patch
# User nipkow
# Date 1224539597 -7200
# Node ID caa1137d25dca829a87049fdb4d3f6171aad5173
# Parent  658b598d8af4eebf95402596cb2ff52ce4e1367a
fixed proof

diff -r 658b598d8af4 -r caa1137d25dc src/HOL/Word/WordDefinition.thy
--- a/src/HOL/Word/WordDefinition.thy	Mon Oct 20 23:52:59 2008 +0200
+++ b/src/HOL/Word/WordDefinition.thy	Mon Oct 20 23:53:17 2008 +0200
@@ -830,10 +830,7 @@
 lemma ucast_up_app': 
   "uc = ucast ==> source_size uc + n = target_size uc ==> 
     to_bl (uc w) = replicate n False @ (to_bl w)"
-  apply (auto simp add : source_size target_size to_bl_ucast)
-  apply (rule_tac f = "%n. replicate n False" in arg_cong)
-  apply simp
-  done
+  by (auto simp add : source_size target_size to_bl_ucast)
 
 lemma ucast_down_drop': 
   "uc = ucast ==> source_size uc = target_size uc + n ==> 
diff -r 658b598d8af4 -r caa1137d25dc src/HOL/Word/WordShift.thy
--- a/src/HOL/Word/WordShift.thy	Mon Oct 20 23:52:59 2008 +0200
+++ b/src/HOL/Word/WordShift.thy	Mon Oct 20 23:53:17 2008 +0200
@@ -458,7 +458,6 @@
    apply (simp add: bl_word_and to_bl_0)
    apply (rule align_lem_and [THEN trans])
        apply (simp_all add: word_size)[5]
-   apply (rule_tac f = "%n. replicate n False" in arg_cong)
    apply simp
   apply (subst word_plus_and_or [symmetric])
   apply (simp add : bl_word_or)
@@ -710,8 +709,6 @@
   apply (rule bl_shiftl [THEN trans])
   apply (subst ucast_up_app)
   apply (auto simp add: wsst_TYs)
-  apply (drule sym)
-  apply (simp add: min_def)
   done
 
 lemmas revcast_up = refl [THEN revcast_up']