src/HOL/Word/Word_Miscellaneous.thy

--- a/src/HOL/Word/Word_Miscellaneous.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Word/Word_Miscellaneous.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -3,7 +3,7 @@
 section \<open>Miscellaneous lemmas, of at least doubtful value\<close>
 
 theory Word_Miscellaneous
-  imports "~~/src/HOL/Library/Bit" Misc_Numeric
+  imports "HOL-Library.Bit" Misc_Numeric
 begin
 
 lemma power_minus_simp: "0 < n \<Longrightarrow> a ^ n = a * a ^ (n - 1)"