fixed proof: no one_is_Suc_zero;
authorwenzelm
Mon Oct 22 21:32:09 2007 +0200 (2007-10-22)
changeset 25149776f985efa4c
parent 25148 9c9646c1080d
child 25150 9d8893e9f381
fixed proof: no one_is_Suc_zero;
src/HOL/Word/WordDefinition.thy
     1.1 --- a/src/HOL/Word/WordDefinition.thy	Mon Oct 22 21:32:06 2007 +0200
     1.2 +++ b/src/HOL/Word/WordDefinition.thy	Mon Oct 22 21:32:09 2007 +0200
     1.3 @@ -414,7 +414,7 @@
     1.4  lemma sint_sbintrunc: "sint (number_of bin :: 'a word) = 
     1.5      number_of (sbintrunc (len_of TYPE ('a :: len) - 1) bin)" 
     1.6    unfolding word_number_of_def number_of_eq
     1.7 -  by (auto intro!: word_sbin.eq_norm simp del: one_is_Suc_zero)
     1.8 +  by (subst word_sbin.eq_norm) simp
     1.9  
    1.10  lemma unat_bintrunc: 
    1.11    "unat (number_of bin :: 'a :: len0 word) =