diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Word/Bits_Bit.thy --- 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 \Bit operations in $\cal Z_2$\ theory Bits_Bit -imports Bits "~~/src/HOL/Library/Bit" +imports Bits "HOL-Library.Bit" begin instantiation bit :: bit