src/HOL/SPARK/Manual/Reference.thy
changeset 66992 69673025292e
parent 66453 cc19f7ca2ed6
child 69597 ff784d5a5bfb
--- a/src/HOL/SPARK/Manual/Reference.thy	Thu Nov 02 15:21:35 2017 +0100
+++ b/src/HOL/SPARK/Manual/Reference.thy	Fri Nov 03 13:43:31 2017 +0100
@@ -1,6 +1,6 @@
 (*<*)
 theory Reference
-imports SPARK
+imports "HOL-SPARK.SPARK"
 begin
 
 syntax (my_constrain output)