src/HOL/Word/WordMain.thy
author wenzelm
Wed Sep 17 21:27:14 2008 +0200 (2008-09-17)
changeset 28263 69eaa97e7e96
parent 27137 d0070c32fdc1
permissions -rw-r--r--
moved global ML bindings to global place;
     1 (* 
     2   ID:     $Id$
     3   Author: Gerwin Klein, NICTA
     4 
     5   The main interface of the word library to other theories.
     6 *)
     7 
     8 header {* Main Word Library *}
     9 
    10 theory WordMain
    11 imports WordGenLib
    12 begin
    13 
    14 lemmas word_no_1 [simp] = word_1_no [symmetric, unfolded BIT_simps]
    15 lemmas word_no_0 [simp] = word_0_no [symmetric]
    16 
    17 declare word_0_bl [simp]
    18 declare bin_to_bl_def [simp]
    19 declare to_bl_0 [simp]
    20 declare of_bl_True [simp]
    21 
    22 text "Examples"
    23 
    24 types word32 = "32 word"
    25 types word8 = "8 word"
    26 types byte = word8
    27 
    28 text {* for more see WordExamples.thy *}
    29 
    30 end