| changeset 71956 | a4bffc0de967 |
| parent 71954 | 13bb3f5cdc5b |
| child 71965 | d45f5d4c41bd |
| 71955:a9f913d17d00 | 71956:a4bffc0de967 |
|---|---|
5 |
5 |
6 theory Word |
6 theory Word |
7 imports |
7 imports |
8 Main |
8 Main |
9 "HOL-Library.Type_Length" |
9 "HOL-Library.Type_Length" |
10 "HOL-ex.Bit_Operations" |
10 "HOL-Library.Bit_Operations" |
11 begin |
11 begin |
12 |
12 |
13 subsection \<open>Preliminaries\<close> |
13 subsection \<open>Preliminaries\<close> |
14 |
14 |
15 definition signed_take_bit :: "nat \<Rightarrow> int \<Rightarrow> int" |
15 definition signed_take_bit :: "nat \<Rightarrow> int \<Rightarrow> int" |