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.
recovered example types from WordMain.thy;
authorwenzelm
Tue, 27 Jan 2009 13:41:45 +0100
changeset 29640 741f26190c96
parent 29637 da018485b89d
child 29641 08d462dbb1a9
recovered example types from WordMain.thy;
src/HOL/Word/Examples/WordExamples.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle