src/HOL/Word/Examples/WordExamples.thy
changeset 42463 f270e3e18be5
parent 29640 741f26190c96
child 44762 8f9d09241a68
     1.1 --- a/src/HOL/Word/Examples/WordExamples.thy	Fri Apr 22 15:57:43 2011 +0200
     1.2 +++ b/src/HOL/Word/Examples/WordExamples.thy	Sat Apr 23 13:00:19 2011 +0200
     1.3 @@ -10,9 +10,9 @@
     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 +type_synonym word32 = "32 word"
    1.11 +type_synonym word8 = "8 word"
    1.12 +type_synonym byte = word8
    1.13  
    1.14  -- "modulus"
    1.15