# HG changeset patch
# User wenzelm
# Date 1193081529 -7200
# Node ID 776f985efa4c54d7ed5cff723fbecc76adb8a958
# Parent  9c9646c1080d673c5c1149aef0f3a0afa3d1705f
fixed proof: no one_is_Suc_zero;

diff -r 9c9646c1080d -r 776f985efa4c src/HOL/Word/WordDefinition.thy
--- a/src/HOL/Word/WordDefinition.thy	Mon Oct 22 21:32:06 2007 +0200
+++ b/src/HOL/Word/WordDefinition.thy	Mon Oct 22 21:32:09 2007 +0200
@@ -414,7 +414,7 @@
 lemma sint_sbintrunc: "sint (number_of bin :: 'a word) = 
     number_of (sbintrunc (len_of TYPE ('a :: len) - 1) bin)" 
   unfolding word_number_of_def number_of_eq
-  by (auto intro!: word_sbin.eq_norm simp del: one_is_Suc_zero)
+  by (subst word_sbin.eq_norm) simp
 
 lemma unat_bintrunc: 
   "unat (number_of bin :: 'a :: len0 word) =