src/HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy
changeset 55818 d8b2f50705d0
parent 41588 9546828c0eb3
child 66453 cc19f7ca2ed6
--- a/src/HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy	Sat Mar 01 09:34:08 2014 +0100
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy	Sat Mar 01 17:08:39 2014 +0100
@@ -5,7 +5,7 @@
 *)
 
 theory RMD_Specification
-imports RMD SPARK
+imports RMD "~~/src/HOL/SPARK/SPARK"
 begin
 
 (* bit operations *)