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;
kleing@24333
     1
(* 
kleing@24333
     2
  ID:     $Id$
kleing@24333
     3
  Author: Gerwin Klein, NICTA
kleing@24333
     4
kleing@24333
     5
  The main interface of the word library to other theories.
kleing@24333
     6
*)
kleing@24333
     7
huffman@24350
     8
header {* Main Word Library *}
huffman@24350
     9
haftmann@26560
    10
theory WordMain
haftmann@26560
    11
imports WordGenLib
kleing@24333
    12
begin
kleing@24333
    13
huffman@26086
    14
lemmas word_no_1 [simp] = word_1_no [symmetric, unfolded BIT_simps]
kleing@24333
    15
lemmas word_no_0 [simp] = word_0_no [symmetric]
kleing@24333
    16
kleing@24333
    17
declare word_0_bl [simp]
kleing@24333
    18
declare bin_to_bl_def [simp]
kleing@24333
    19
declare to_bl_0 [simp]
kleing@24333
    20
declare of_bl_True [simp]
kleing@24333
    21
kleing@24333
    22
text "Examples"
kleing@24333
    23
kleing@24333
    24
types word32 = "32 word"
kleing@24333
    25
types word8 = "8 word"
kleing@24333
    26
types byte = word8
kleing@24333
    27
wenzelm@27137
    28
text {* for more see WordExamples.thy *}
kleing@24333
    29
kleing@24333
    30
end