--- a/src/HOL/Isar_examples/ROOT.ML Fri Aug 10 18:21:25 2007 +0200
+++ b/src/HOL/Isar_examples/ROOT.ML Fri Aug 10 22:31:19 2007 +0200
@@ -5,17 +5,19 @@
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
*)
-time_use_thy "BasicLogic";
-time_use_thy "Cantor";
-time_use_thy "Peirce";
-time_use_thy "Drinker";
-time_use_thy "ExprCompiler";
-time_use_thy "Group";
-time_use_thy "Summation";
-time_use_thy "KnasterTarski";
-time_use_thy "MutilatedCheckerboard";
-with_path "../NumberTheory" (no_document time_use_thy) "Primes";
-with_path "../NumberTheory" time_use_thy "Fibonacci";
-time_use_thy "Puzzle";
-time_use_thy "NestedDatatype";
-time_use_thy "HoareEx";
+no_document use_thys ["../NumberTheory/Primes", "../NumberTheory/Fibonacci"];
+
+use_thys [
+ "BasicLogic",
+ "Cantor",
+ "Peirce",
+ "Drinker",
+ "ExprCompiler",
+ "Group",
+ "Summation",
+ "KnasterTarski",
+ "MutilatedCheckerboard",
+ "Puzzle",
+ "NestedDatatype",
+ "HoareEx"
+];