included meson/metis tests in simultaneous use_thys;
authorwenzelm
Thu, 20 Dec 2007 22:21:30 +0100
changeset 25738 b091cbae3e2a
parent 25737 84c92fc48e36
child 25739 9da2343deb92
included meson/metis tests in simultaneous use_thys;
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";