# HG changeset patch
# User haftmann
# Date 1233004456 -3600
# Node ID d9294387ab0eef0022b5e124b9444a2e07009857
# Parent  152ace41f3fbdeae59bd62a6cd833ee79270c628
entry point for Word library now named Word

diff -r 152ace41f3fb -r d9294387ab0e NEWS
--- a/NEWS	Mon Jan 26 08:23:55 2009 +0100
+++ b/NEWS	Mon Jan 26 22:14:16 2009 +0100
@@ -193,6 +193,8 @@
 
 *** HOL ***
 
+* Entry point to Word library now simply named "Word".  INCOMPATIBILITY.
+
 * Made source layout more coherent with logical distribution
 structure:
 
diff -r 152ace41f3fb -r d9294387ab0e src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Jan 26 08:23:55 2009 +0100
+++ b/src/HOL/IsaMakefile	Mon Jan 26 22:14:16 2009 +0100
@@ -974,7 +974,7 @@
   Word/Size.thy Word/BinGeneral.thy Word/BinOperations.thy		\
   Word/BinBoolList.thy Word/BitSyntax.thy Word/WordDefinition.thy	\
   Word/WordArith.thy Word/WordBitwise.thy Word/WordShift.thy		\
-  Word/WordGenLib.thy Word/WordMain.thy Word/document/root.tex		\
+  Word/WordGenLib.thy Word/Word.thy Word/document/root.tex		\
   Word/document/root.bib
 	@cd Word; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Word
 
diff -r 152ace41f3fb -r d9294387ab0e src/HOL/Word/ROOT.ML
--- a/src/HOL/Word/ROOT.ML	Mon Jan 26 08:23:55 2009 +0100
+++ b/src/HOL/Word/ROOT.ML	Mon Jan 26 22:14:16 2009 +0100
@@ -1,2 +1,1 @@
-no_document use_thys ["Infinite_Set"];
-use_thy "WordMain";
+use_thy "Word";
diff -r 152ace41f3fb -r d9294387ab0e src/HOL/Word/Word.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Word/Word.thy	Mon Jan 26 22:14:16 2009 +0100
@@ -0,0 +1,13 @@
+(*  Title:      HOL/Word/Word.thy
+    Author:     Gerwin Klein, NICTA
+*)
+
+header {* Word Library interafce *}
+
+theory Word
+imports WordGenLib
+begin
+
+text {* see @{text "Examples/WordExamples.thy"} for examples *}
+
+end
diff -r 152ace41f3fb -r d9294387ab0e src/HOL/Word/WordGenLib.thy
--- a/src/HOL/Word/WordGenLib.thy	Mon Jan 26 08:23:55 2009 +0100
+++ b/src/HOL/Word/WordGenLib.thy	Mon Jan 26 22:14:16 2009 +0100
@@ -1,5 +1,4 @@
 (* Author: Gerwin Klein, Jeremy Dawson
-   $Id$
 
    Miscellaneous additional library definitions and lemmas for 
    the word type. Instantiation to boolean algebras, definition
@@ -452,4 +451,13 @@
   "1 + n \<noteq> (0::'a::len word) \<Longrightarrow> unat (1 + n) = Suc (unat n)"
   by unat_arith
 
+
+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]
+
 end