--- a/src/HOL/Word/Bits_Int.thy Tue Sep 15 08:57:47 2020 +0200
+++ b/src/HOL/Word/Bits_Int.thy Thu Sep 17 09:57:30 2020 +0000
@@ -372,11 +372,11 @@
lemma sbintrunc_inc:
\<open>k + 2 ^ Suc n \<le> sbintrunc n k\<close> if \<open>k < - (2 ^ n)\<close>
- using that by (fact signed_take_bit_greater_eq)
+ using that by (fact signed_take_bit_int_greater_eq)
lemma sbintrunc_dec:
\<open>sbintrunc n k \<le> k - 2 ^ (Suc n)\<close> if \<open>k \<ge> 2 ^ n\<close>
- using that by (fact signed_take_bit_less_eq)
+ using that by (fact signed_take_bit_int_less_eq)
lemma bintr_ge0: "0 \<le> bintrunc n w"
by (simp add: bintrunc_mod2p)