# HG changeset patch
# User wenzelm
# Date 1198185690 -3600
# Node ID b091cbae3e2acc41991eaeec1475cd034d70ddc0
# Parent  84c92fc48e363ed0c947ebbe961634d1c13ff4a4
included meson/metis tests in simultaneous use_thys;

diff -r 84c92fc48e36 -r b091cbae3e2a src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Thu Dec 20 21:14:28 2007 +0100
+++ b/src/HOL/ex/ROOT.ML	Thu Dec 20 22:21:30 2007 +0100
@@ -53,15 +53,14 @@
   "Random",
   "Primrec",
   "Tarski",
-  "Adder"
+  "Adder",
+  "Classical",
+  "set",
+  "Meson_Test"
 ];
 
 setmp Proofterm.proofs 2 time_use_thy "Hilbert_Classical";
 
-time_use_thy "Classical";
-time_use_thy "set";
-
-time_use_thy "Meson_Test";
 time_use_thy "Dense_Linear_Order_Ex";
 time_use_thy "PresburgerEx";
 time_use_thy "Reflected_Presburger";