src/HOLCF/IOA/ex/ROOT.ML
changeset 33615 261abc2e3155
parent 24584 01e83ffa6c54
equal deleted inserted replaced
33608:5c0024338cef 33615:261abc2e3155
     1 (*  Title:      HOLCF/IOA/ex/ROOT.ML
     1 (*  Title:      HOLCF/IOA/ex/ROOT.ML
     2     ID:         $Id$
       
     3     Author:     Olaf Mueller
     2     Author:     Olaf Mueller
     4 *)
     3 *)
     5 
     4 
     6 time_use_thy "TrivEx";
     5 use_thys ["TrivEx", "TrivEx2"];
     7 time_use_thy "TrivEx2";