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