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