# HG changeset patch
# User haftmann
# Date 1233004491 -3600
# Node ID 3eb52e5a90a00917e4348060459f50f132749c33
# Parent  c3d576157244effffbc8001d14187f4e19921a6a
entry point for Word library now named Word

diff -r c3d576157244 -r 3eb52e5a90a0 src/HOL/Word/WordMain.thy
--- a/src/HOL/Word/WordMain.thy	Mon Jan 26 22:14:19 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,30 +0,0 @@
-(* 
-  ID:     $Id$
-  Author: Gerwin Klein, NICTA
-
-  The main interface of the word library to other theories.
-*)
-
-header {* Main Word Library *}
-
-theory WordMain
-imports WordGenLib
-begin
-
-lemmas word_no_1 [simp] = word_1_no [symmetric, unfolded BIT_simps]
-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 WordExamples.thy *}
-
-end