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