equal
deleted
inserted
replaced
521 |
521 |
522 lemma shiftl0: |
522 lemma shiftl0: |
523 "x << 0 = (x :: 'a :: len word)" |
523 "x << 0 = (x :: 'a :: len word)" |
524 by (fact shiftl_x_0) |
524 by (fact shiftl_x_0) |
525 |
525 |
526 setup \<open> |
|
527 Context.theory_map (fold SMT_Word.add_word_shift' [ |
|
528 (\<^term>\<open>shiftl :: 'a::len word \<Rightarrow> _\<close>, "bvshl"), |
|
529 (\<^term>\<open>shiftr :: 'a::len word \<Rightarrow> _\<close>, "bvlshr"), |
|
530 (\<^term>\<open>sshiftr :: 'a::len word \<Rightarrow> _\<close>, "bvashr") |
|
531 ]) |
|
532 \<close> |
|
533 |
|
534 end |
526 end |