| changeset 71418 | bd9d27ccb3a3 |
| parent 71413 | 65ffe9e910d4 |
| child 71424 | e83fe2c31088 |
--- 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 \<Rightarrow> '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 \<Rightarrow> 'a word \<Rightarrow> 'a word" is \<open>and\<close>