| author | ballarin |
| Fri, 19 Dec 2008 16:39:23 +0100 | |
| changeset 29249 | 4dc278c8dc59 |
| parent 27137 | d0070c32fdc1 |
| 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 |
||
| 26560 | 10 |
theory WordMain |
11 |
imports WordGenLib |
|
| 24333 | 12 |
begin |
13 |
||
|
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
24350
diff
changeset
|
14 |
lemmas word_no_1 [simp] = word_1_no [symmetric, unfolded BIT_simps] |
| 24333 | 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 |
||
|
27137
d0070c32fdc1
fixed spelling (Where is WordExamples.thy anyway?);
wenzelm
parents:
26560
diff
changeset
|
28 |
text {* for more see WordExamples.thy *}
|
| 24333 | 29 |
|
30 |
end |