equal
deleted
inserted
replaced
5 contains theorems to do with shifting, rotating, splitting words |
5 contains theorems to do with shifting, rotating, splitting words |
6 *) |
6 *) |
7 |
7 |
8 header {* Shifting, Rotating, and Splitting Words *} |
8 header {* Shifting, Rotating, and Splitting Words *} |
9 |
9 |
10 theory WordShift imports WordBitwise begin |
10 theory WordShift imports WordBitwise WordBoolList begin |
11 |
11 |
12 subsection "Bit shifting" |
12 subsection "Bit shifting" |
13 |
13 |
14 constdefs |
14 constdefs |
15 shiftl1 :: "'a :: len0 word => 'a word" |
15 shiftl1 :: "'a :: len0 word => 'a word" |