changeset 66453 | cc19f7ca2ed6 |
parent 65363 | 5eb619751b14 |
child 67120 | 491fd7f0b5df |
--- a/src/HOL/Word/Bits_Bit.thy Fri Aug 18 13:55:05 2017 +0200 +++ b/src/HOL/Word/Bits_Bit.thy Fri Aug 18 20:47:47 2017 +0200 @@ -5,7 +5,7 @@ section \<open>Bit operations in $\cal Z_2$\<close> theory Bits_Bit -imports Bits "~~/src/HOL/Library/Bit" +imports Bits "HOL-Library.Bit" begin instantiation bit :: bit