entry point for Word library now named Word
authorhaftmann
Mon Jan 26 22:14:16 2009 +0100 (2009-01-26)
changeset 29628d9294387ab0e
parent 29627 152ace41f3fb
child 29629 5111ce425e7a
entry point for Word library now named Word
NEWS
src/HOL/IsaMakefile
src/HOL/Word/ROOT.ML
src/HOL/Word/Word.thy
src/HOL/Word/WordGenLib.thy
     1.1 --- a/NEWS	Mon Jan 26 08:23:55 2009 +0100
     1.2 +++ b/NEWS	Mon Jan 26 22:14:16 2009 +0100
     1.3 @@ -193,6 +193,8 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Entry point to Word library now simply named "Word".  INCOMPATIBILITY.
     1.8 +
     1.9  * Made source layout more coherent with logical distribution
    1.10  structure:
    1.11  
     2.1 --- a/src/HOL/IsaMakefile	Mon Jan 26 08:23:55 2009 +0100
     2.2 +++ b/src/HOL/IsaMakefile	Mon Jan 26 22:14:16 2009 +0100
     2.3 @@ -974,7 +974,7 @@
     2.4    Word/Size.thy Word/BinGeneral.thy Word/BinOperations.thy		\
     2.5    Word/BinBoolList.thy Word/BitSyntax.thy Word/WordDefinition.thy	\
     2.6    Word/WordArith.thy Word/WordBitwise.thy Word/WordShift.thy		\
     2.7 -  Word/WordGenLib.thy Word/WordMain.thy Word/document/root.tex		\
     2.8 +  Word/WordGenLib.thy Word/Word.thy Word/document/root.tex		\
     2.9    Word/document/root.bib
    2.10  	@cd Word; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Word
    2.11  
     3.1 --- a/src/HOL/Word/ROOT.ML	Mon Jan 26 08:23:55 2009 +0100
     3.2 +++ b/src/HOL/Word/ROOT.ML	Mon Jan 26 22:14:16 2009 +0100
     3.3 @@ -1,2 +1,1 @@
     3.4 -no_document use_thys ["Infinite_Set"];
     3.5 -use_thy "WordMain";
     3.6 +use_thy "Word";
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Word/Word.thy	Mon Jan 26 22:14:16 2009 +0100
     4.3 @@ -0,0 +1,13 @@
     4.4 +(*  Title:      HOL/Word/Word.thy
     4.5 +    Author:     Gerwin Klein, NICTA
     4.6 +*)
     4.7 +
     4.8 +header {* Word Library interafce *}
     4.9 +
    4.10 +theory Word
    4.11 +imports WordGenLib
    4.12 +begin
    4.13 +
    4.14 +text {* see @{text "Examples/WordExamples.thy"} for examples *}
    4.15 +
    4.16 +end
     5.1 --- a/src/HOL/Word/WordGenLib.thy	Mon Jan 26 08:23:55 2009 +0100
     5.2 +++ b/src/HOL/Word/WordGenLib.thy	Mon Jan 26 22:14:16 2009 +0100
     5.3 @@ -1,5 +1,4 @@
     5.4  (* Author: Gerwin Klein, Jeremy Dawson
     5.5 -   $Id$
     5.6  
     5.7     Miscellaneous additional library definitions and lemmas for 
     5.8     the word type. Instantiation to boolean algebras, definition
     5.9 @@ -452,4 +451,13 @@
    5.10    "1 + n \<noteq> (0::'a::len word) \<Longrightarrow> unat (1 + n) = Suc (unat n)"
    5.11    by unat_arith
    5.12  
    5.13 +
    5.14 +lemmas word_no_1 [simp] = word_1_no [symmetric, unfolded BIT_simps]
    5.15 +lemmas word_no_0 [simp] = word_0_no [symmetric]
    5.16 +
    5.17 +declare word_0_bl [simp]
    5.18 +declare bin_to_bl_def [simp]
    5.19 +declare to_bl_0 [simp]
    5.20 +declare of_bl_True [simp]
    5.21 +
    5.22  end