src/HOL/Word/WordMain.thy

* HOL-Word:
New extensive library and type for generic, fixed size machine
words, with arithemtic, bit-wise, shifting and rotating operations,
reflection into int, nat, and bool lists, automation for linear
arithmetic (by automatic reflection into nat or int), including
lemmas on overflow and monotonicity. Instantiated to all appropriate
arithmetic type classes, supporting automatic simplification of
numerals on all operations. Jointly developed by NICTA, Galois, and
PSU.

* still to do: README.html/document + moving some of the generic lemmas
to appropriate place in distribution

(* 
  ID:     $Id$
  Author: Gerwin Klein, NICTA

  The main interface of the word library to other theories.
*)

theory WordMain imports WordGenLib
begin

lemmas word_no_1 [simp] = word_1_no [symmetric]
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 WordExampes.thy *}

end