src/HOL/Imperative_HOL/ROOT.ML
changeset 30689 b14b2cc4e25e
parent 29399 ebcd69a00872
child 33615 261abc2e3155
--- a/src/HOL/Imperative_HOL/ROOT.ML	Mon Mar 23 19:01:17 2009 +0100
+++ b/src/HOL/Imperative_HOL/ROOT.ML	Mon Mar 23 19:01:17 2009 +0100
@@ -1,2 +1,2 @@
 
-use_thy "Imperative_HOL";
+use_thy "Imperative_HOL_ex";