src/HOL/Imperative_HOL/Imperative_HOL_ex.thy
changeset 39307 8d42d668b5b0
parent 38058 e4640c2ceb43
child 50630 1ea90e8046dc
--- a/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy	Mon Sep 13 14:54:02 2010 +0200
+++ b/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy	Mon Sep 13 14:54:05 2010 +0200
@@ -6,7 +6,7 @@
 header {* Monadic imperative HOL with examples *}
 
 theory Imperative_HOL_ex
-imports Imperative_HOL
+imports Imperative_HOL Overview
   "ex/Imperative_Quicksort" "ex/Imperative_Reverse" "ex/Linked_Lists" "ex/SatChecker"
 begin