# HG changeset patch
# User wenzelm
# Date 1233060105 -3600
# Node ID 741f26190c96a542c5be03c5d723618b0c7fea2d
# Parent  da018485b89d4d8a786e15ac055311506773cca4
recovered example types from WordMain.thy;

diff -r da018485b89d -r 741f26190c96 src/HOL/Word/Examples/WordExamples.thy
--- 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