# HG changeset patch
# User wenzelm
# Date 1233060752 -3600
# Node ID 08d462dbb1a9ded103c641d13aa04dd41073a5f8
# Parent  741f26190c96a542c5be03c5d723618b0c7fea2d# Parent  b9a7ea6c6da7c739604a7f22306167d848feee84
merged

diff -r b9a7ea6c6da7 -r 08d462dbb1a9 src/HOL/Word/Examples/WordExamples.thy
--- a/src/HOL/Word/Examples/WordExamples.thy	Tue Jan 27 12:59:38 2009 +0100
+++ b/src/HOL/Word/Examples/WordExamples.thy	Tue Jan 27 13:52:32 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