src/HOL/Word/WordMain.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Word/WordMain.thy	Mon Aug 20 04:34:31 2007 +0200
@@ -0,0 +1,27 @@
+(* 
+  ID:     $Id$
+  Author: Gerwin Klein, NICTA
+
+  The main interface of the word library to other theories.
+*)
+
+theory WordMain imports WordGenLib
+begin
+
+lemmas word_no_1 [simp] = word_1_no [symmetric]
+lemmas word_no_0 [simp] = word_0_no [symmetric]
+
+declare word_0_bl [simp]
+declare bin_to_bl_def [simp]
+declare to_bl_0 [simp]
+declare of_bl_True [simp]
+
+text "Examples"
+
+types word32 = "32 word"
+types word8 = "8 word"
+types byte = word8
+
+text {* for more see WordExampes.thy *}
+
+end