src/HOL/SPARK/Manual/Reference.thy
changeset 72488 ee659bca8955
parent 69597 ff784d5a5bfb
child 72514 d8661799afb2
--- a/src/HOL/SPARK/Manual/Reference.thy	Thu Oct 15 14:55:19 2020 +0200
+++ b/src/HOL/SPARK/Manual/Reference.thy	Sat Oct 17 18:56:36 2020 +0200
@@ -1,6 +1,6 @@
 (*<*)
 theory Reference
-imports "HOL-SPARK.SPARK"
+imports "HOL-SPARK.SPARK" "HOL-Word.Bits_Int"
 begin
 
 syntax (my_constrain output)