1.1 --- a/src/HOL/ex/ROOT.ML	Tue Nov 10 13:05:35 2009 +0100
     1.2 +++ b/src/HOL/ex/ROOT.ML	Tue Nov 10 13:17:50 2009 +0100
     1.3 @@ -67,6 +67,9 @@
     1.4    "Landau"
     1.5  ];
     1.6  
     1.7 +HTML.with_charset "utf-8" (no_document use_thys)
     1.8 +  ["Hebrew", "Chinese", "Serbian"];
     1.9 +
    1.10  (setmp_noncritical proofs 2 (setmp_noncritical Goal.parallel_proofs 0 use_thy))
    1.11    "Hilbert_Classical";
    1.12  
    1.13 @@ -74,12 +77,10 @@
    1.14  if getenv "SVC_HOME" = "" then ()
    1.15  else use_thy "svc_test";
    1.16  
    1.17 -(*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
    1.18 -try use_thy "SAT_Examples";
    1.19 -
    1.20  (*requires zChaff (or some other reasonably fast SAT solver)*)
    1.21  if getenv "ZCHAFF_HOME" = "" then ()
    1.22  else use_thy "Sudoku";
    1.23  
    1.24 -HTML.with_charset "utf-8" (no_document use_thys)
    1.25 -  ["Hebrew", "Chinese", "Serbian"];
    1.26 +(*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
    1.27 +(*global side-effects ahead!*)
    1.28 +try use_thy "SAT_Examples";   (* FIXME try!? (not really a proper test) *)