--- a/src/HOL/SPARK/Examples/Sqrt/Sqrt.thy Thu Nov 02 15:21:35 2017 +0100
+++ b/src/HOL/SPARK/Examples/Sqrt/Sqrt.thy Fri Nov 03 13:43:31 2017 +0100
@@ -4,7 +4,7 @@
*)
theory Sqrt
-imports SPARK
+imports "HOL-SPARK.SPARK"
begin
spark_open "sqrt/isqrt"