diff -r 89d05db6dd1f -r bd9d27ccb3a3 src/HOL/ex/Word.thy --- a/src/HOL/ex/Word.thy Tue Feb 04 16:19:15 2020 +0000 +++ b/src/HOL/ex/Word.thy Mon Feb 03 20:42:04 2020 +0000 @@ -674,7 +674,7 @@ lift_definition not_word :: "'a word \ 'a word" is not - by (simp add: take_bit_not_iff_int) + by (simp add: take_bit_not_iff) lift_definition and_word :: "'a word \ 'a word \ 'a word" is \and\