| changeset 74097 | 6d7be1227d02 |
| parent 72515 | c7038c397ae3 |
| 74096:cb64ccdc3ac1 | 74097:6d7be1227d02 |
|---|---|
6 |
6 |
7 theory RMD |
7 theory RMD |
8 imports "HOL-Library.Word" |
8 imports "HOL-Library.Word" |
9 begin |
9 begin |
10 |
10 |
11 unbundle bit_operations_syntax |
|
11 |
12 |
12 \<comment> \<open>all operations are defined on 32-bit words\<close> |
13 \<comment> \<open>all operations are defined on 32-bit words\<close> |
13 |
14 |
14 type_synonym word32 = "32 word" |
15 type_synonym word32 = "32 word" |
15 type_synonym byte = "8 word" |
16 type_synonym byte = "8 word" |