changeset 72388 | 633d14bd1e59 |
parent 72292 | 4a58c38b85ff |
child 72397 | 48013583e8e6 |
--- a/src/HOL/Word/More_Word.thy Wed Oct 07 11:31:51 2020 +0200 +++ b/src/HOL/Word/More_Word.thy Wed Oct 07 10:39:14 2020 +0200 @@ -26,7 +26,7 @@ lemmas shiftl1_def = shiftl1_eq lemmas shiftr1_def = shiftr1_eq lemmas sshiftr1_def = sshiftr1_eq -lemmas sshiftr_def = sshiftr_eq +lemmas sshiftr_def = sshiftr_eq_funpow_sshiftr1 lemmas to_bl_def = to_bl_eq lemmas ucast_def = ucast_eq lemmas unat_def = unat_eq_nat_uint