--- 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:
--- 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
--- 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";
--- /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
--- 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