# HG changeset patch
# User wenzelm
# Date 1202761931 -3600
# Node ID 279016aebc411cdd582377fd81c57d4ebd138eaa
# Parent  f5d5c4922cdf863de3adb491cd3962081dddd782
simultaneous use_thys;

diff -r f5d5c4922cdf -r 279016aebc41 src/ZF/ROOT.ML
--- a/src/ZF/ROOT.ML	Mon Feb 11 21:32:10 2008 +0100
+++ b/src/ZF/ROOT.ML	Mon Feb 11 21:32:11 2008 +0100
@@ -8,6 +8,5 @@
 Paulson.
 *)
 
-use_thy "Main";
-use_thy "Main_ZFC";
+use_thys ["Main", "Main_ZFC"];