--- 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 ==>
--- 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']