| changeset 29640 | 741f26190c96 |
| parent 29629 | 5111ce425e7a |
| child 42463 | f270e3e18be5 |
--- a/src/HOL/Word/Examples/WordExamples.thy Tue Jan 27 12:57:24 2009 +0100 +++ b/src/HOL/Word/Examples/WordExamples.thy Tue Jan 27 13:41:45 2009 +0100 @@ -10,6 +10,10 @@ imports Word begin +types word32 = "32 word" +types word8 = "8 word" +types byte = word8 + -- "modulus" lemma "(27 :: 4 word) = -5" by simp