Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authorwenzelm
Tue, 27 Jan 2009 13:52:32 +0100
changeset 29641 08d462dbb1a9
parent 29640 741f26190c96 (diff)
parent 29639 b9a7ea6c6da7 (current diff)
child 29642 be22ba214475
merged
--- 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
isabelle