src/HOL/Word/Word.thy
changeset 59094 9ced35b4a2a9
parent 58963 26bf09b95dda
child 59487 adaa430fc0f7
     1.1 --- a/src/HOL/Word/Word.thy	Fri Dec 05 13:39:59 2014 +0100
     1.2 +++ b/src/HOL/Word/Word.thy	Thu Dec 04 16:51:54 2014 +0100
     1.3 @@ -63,7 +63,6 @@
     1.4    fix x :: "'a word"
     1.5    assume "\<And>x. PROP P (word_of_int x)"
     1.6    then have "PROP P (word_of_int (uint x))" .
     1.7 -  find_theorems word_of_int uint
     1.8    then show "PROP P x" by (simp add: word_of_int_uint)
     1.9  qed
    1.10