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