src/HOL/SPARK/Examples/RIPEMD-160/RMD.thy
changeset 55818 d8b2f50705d0
parent 41587 e13df75fee79
child 62390 842917225d56
--- a/src/HOL/SPARK/Examples/RIPEMD-160/RMD.thy	Sat Mar 01 09:34:08 2014 +0100
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/RMD.thy	Sat Mar 01 17:08:39 2014 +0100
@@ -5,7 +5,7 @@
 *)
 
 theory RMD
-imports Word
+imports "~~/src/HOL/Word/Word"
 begin