--- a/src/HOL/SPARK/Examples/Sqrt/Sqrt.thy Mon Sep 01 17:34:03 2014 +0200 +++ b/src/HOL/SPARK/Examples/Sqrt/Sqrt.thy Mon Sep 01 18:42:02 2014 +0200 @@ -4,7 +4,7 @@ *) theory Sqrt -imports SPARK +imports "../../SPARK" begin spark_open "sqrt/isqrt"