--- a/src/HOL/ex/ROOT.ML Tue Nov 10 13:05:35 2009 +0100
+++ b/src/HOL/ex/ROOT.ML Tue Nov 10 13:17:50 2009 +0100
@@ -67,6 +67,9 @@
"Landau"
];
+HTML.with_charset "utf-8" (no_document use_thys)
+ ["Hebrew", "Chinese", "Serbian"];
+
(setmp_noncritical proofs 2 (setmp_noncritical Goal.parallel_proofs 0 use_thy))
"Hilbert_Classical";
@@ -74,12 +77,10 @@
if getenv "SVC_HOME" = "" then ()
else use_thy "svc_test";
-(*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
-try use_thy "SAT_Examples";
-
(*requires zChaff (or some other reasonably fast SAT solver)*)
if getenv "ZCHAFF_HOME" = "" then ()
else use_thy "Sudoku";
-HTML.with_charset "utf-8" (no_document use_thys)
- ["Hebrew", "Chinese", "Serbian"];
+(*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
+(*global side-effects ahead!*)
+try use_thy "SAT_Examples"; (* FIXME try!? (not really a proper test) *)