src/LCF/ex/ROOT.ML
changeset 24106 f2965bf954dc
parent 15661 9ef583b08647
child 35762 af3ff2ba4c54
     1.1 --- a/src/LCF/ex/ROOT.ML	Tue Jul 31 22:21:22 2007 +0200
     1.2 +++ b/src/LCF/ex/ROOT.ML	Tue Jul 31 23:23:28 2007 +0200
     1.3 @@ -6,7 +6,4 @@
     1.4  Some examples from Lawrence Paulson's book Logic and Computation.
     1.5  *)
     1.6  
     1.7 -time_use_thy "Ex1";
     1.8 -time_use_thy "Ex2";
     1.9 -time_use_thy "Ex3";
    1.10 -time_use_thy "Ex4";
    1.11 +use_thys ["Ex1", "Ex2", "Ex3", "Ex4"];