src/HOL/Imperative_HOL/Imperative_HOL_ex.thy
changeset 34051 1a82e2e29d67
parent 31872 a564aca741f2
child 36098 53992c639da5
--- a/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy	Wed Dec 09 21:33:50 2009 +0100
+++ b/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy	Thu Dec 10 11:58:26 2009 +0100
@@ -6,7 +6,7 @@
 header {* Monadic imperative HOL with examples *}
 
 theory Imperative_HOL_ex
-imports Imperative_HOL "ex/Imperative_Quicksort"
+imports Imperative_HOL "ex/Imperative_Quicksort" "ex/Imperative_Reverse" "ex/Linked_Lists"
 begin
 
 end