changeset 72262 | a282abb07642 |
parent 72198 | 7ffa26f05c72 |
child 72515 | c7038c397ae3 |
--- a/src/HOL/ex/Bit_Lists.thy Thu Sep 17 09:57:30 2020 +0000 +++ b/src/HOL/ex/Bit_Lists.thy Thu Sep 17 09:57:31 2020 +0000 @@ -5,7 +5,7 @@ theory Bit_Lists imports - "HOL-Word.Conversions" "HOL-Library.More_List" + "HOL-Word.Word" "HOL-Library.More_List" begin subsection \<open>Fragments of algebraic bit representations\<close>