# HG changeset patch
# User wenzelm
# Date 1186777879 -7200
# Node ID 9e2234f2aff12021168248d313ac760ea46c45b9
# Parent  9b226b56e9a9aa2dd0bf42bc19a29c23d65c7189
simultaneous use_thys;

diff -r 9b226b56e9a9 -r 9e2234f2aff1 src/HOL/Isar_examples/ROOT.ML
--- 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"
+];