src/HOL/Imperative_HOL/Imperative_HOL.thy
changeset 37776 df0350f1e7f2
parent 37772 026ed2fc15d4
child 53109 186535065f5c
--- a/src/HOL/Imperative_HOL/Imperative_HOL.thy	Mon Jul 12 16:38:20 2010 +0200
+++ b/src/HOL/Imperative_HOL/Imperative_HOL.thy	Mon Jul 12 16:40:48 2010 +0200
@@ -5,7 +5,7 @@
 header {* Entry point into monadic imperative HOL *}
 
 theory Imperative_HOL
-imports Array Ref Relational Mrec
+imports Array Ref Mrec
 begin
 
 end