author | huffman |
Sun, 17 Feb 2008 06:49:53 +0100 | |
changeset 26086 | 3c243098b64a |
parent 24350 | 4d74f37c6367 |
child 26560 | d2fc9a18ee8a |
permissions | -rw-r--r-- |
24333 | 1 |
(* |
2 |
ID: $Id$ |
|
3 |
Author: Gerwin Klein, NICTA |
|
4 |
||
5 |
The main interface of the word library to other theories. |
|
6 |
*) |
|
7 |
||
24350 | 8 |
header {* Main Word Library *} |
9 |
||
24333 | 10 |
theory WordMain imports WordGenLib |
11 |
begin |
|
12 |
||
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
24350
diff
changeset
|
13 |
lemmas word_no_1 [simp] = word_1_no [symmetric, unfolded BIT_simps] |
24333 | 14 |
lemmas word_no_0 [simp] = word_0_no [symmetric] |
15 |
||
16 |
declare word_0_bl [simp] |
|
17 |
declare bin_to_bl_def [simp] |
|
18 |
declare to_bl_0 [simp] |
|
19 |
declare of_bl_True [simp] |
|
20 |
||
21 |
text "Examples" |
|
22 |
||
23 |
types word32 = "32 word" |
|
24 |
types word8 = "8 word" |
|
25 |
types byte = word8 |
|
26 |
||
27 |
text {* for more see WordExampes.thy *} |
|
28 |
||
29 |
end |