equal
deleted
inserted
replaced
|
1 (* |
|
2 ID: $Id$ |
|
3 Author: Gerwin Klein, NICTA |
|
4 |
|
5 The main interface of the word library to other theories. |
|
6 *) |
|
7 |
|
8 theory WordMain imports WordGenLib |
|
9 begin |
|
10 |
|
11 lemmas word_no_1 [simp] = word_1_no [symmetric] |
|
12 lemmas word_no_0 [simp] = word_0_no [symmetric] |
|
13 |
|
14 declare word_0_bl [simp] |
|
15 declare bin_to_bl_def [simp] |
|
16 declare to_bl_0 [simp] |
|
17 declare of_bl_True [simp] |
|
18 |
|
19 text "Examples" |
|
20 |
|
21 types word32 = "32 word" |
|
22 types word8 = "8 word" |
|
23 types byte = word8 |
|
24 |
|
25 text {* for more see WordExampes.thy *} |
|
26 |
|
27 end |