| changeset 44762 | 8f9d09241a68 |
| parent 42463 | f270e3e18be5 |
| child 46015 | 713c1f396e33 |
| 44761:0694fc3248fd | 44762:8f9d09241a68 |
|---|---|
5 *) |
5 *) |
6 |
6 |
7 header "Examples of word operations" |
7 header "Examples of word operations" |
8 |
8 |
9 theory WordExamples |
9 theory WordExamples |
10 imports Word |
10 imports "../Word" |
11 begin |
11 begin |
12 |
12 |
13 type_synonym word32 = "32 word" |
13 type_synonym word32 = "32 word" |
14 type_synonym word8 = "8 word" |
14 type_synonym word8 = "8 word" |
15 type_synonym byte = word8 |
15 type_synonym byte = word8 |