src/HOL/IMP/ROOT.ML
changeset 24104 719fbe4fb77f
parent 13095 8ed413a57bdc
child 28583 9bb9791bdc18
     1.1 --- a/src/HOL/IMP/ROOT.ML	Tue Jul 31 22:21:18 2007 +0200
     1.2 +++ b/src/HOL/IMP/ROOT.ML	Tue Jul 31 22:21:20 2007 +0200
     1.3 @@ -6,9 +6,4 @@
     1.4  Caveat: HOLCF/IMP depends on HOL/IMP
     1.5  *)
     1.6  
     1.7 -time_use_thy "Expr";
     1.8 -time_use_thy "Transition";
     1.9 -time_use_thy "VC";
    1.10 -time_use_thy "Examples";
    1.11 -time_use_thy "Compiler0";
    1.12 -time_use_thy "Compiler";
    1.13 +use_thys ["Expr", "Transition", "VC", "Examples", "Compiler0", "Compiler"];