author wenzelm
Tue, 10 Jun 2008 21:50:30 +0200
changeset 27137 d0070c32fdc1
parent 26560 d2fc9a18ee8a
permissions -rw-r--r--
fixed spelling (Where is WordExamples.thy anyway?);

  ID:     $Id$
  Author: Gerwin Klein, NICTA

  The main interface of the word library to other theories.

header {* Main Word Library *}

theory WordMain
imports WordGenLib

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 *}