src/HOLCF/ex/ROOT.ML
changeset 24106 f2965bf954dc
parent 18072 102d4ebae879
child 29992 5deee36e33c4
     1.1 --- a/src/HOLCF/ex/ROOT.ML	Tue Jul 31 22:21:22 2007 +0200
     1.2 +++ b/src/HOLCF/ex/ROOT.ML	Tue Jul 31 23:23:28 2007 +0200
     1.3 @@ -4,11 +4,5 @@
     1.4  Misc HOLCF examples.
     1.5  *)
     1.6  
     1.7 -time_use_thy "Dnat";
     1.8 -time_use_thy "Stream";
     1.9 -time_use_thy "Dagstuhl";
    1.10 -time_use_thy "Focus_ex";
    1.11 -time_use_thy "Fix2";
    1.12 -time_use_thy "Hoare";
    1.13 -time_use_thy "Loop";
    1.14 -time_use_thy "Fixrec_ex";
    1.15 +use_thys ["Dnat", "Stream", "Dagstuhl", "Focus_ex", "Fix2", "Hoare",
    1.16 +  "Loop", "Fixrec_ex"];