1.1 --- a/src/HOL/ex/ROOT.ML	Fri Jun 01 16:04:13 2007 +0200
     1.2 +++ b/src/HOL/ex/ROOT.ML	Fri Jun 01 20:34:12 2007 +0200
     1.3 @@ -61,14 +61,15 @@
     1.4  time_use_thy "SVC_Oracle";
     1.5  if_svc_enabled time_use_thy "svc_test";
     1.6  
     1.7 -(* requires zChaff with proof generation to be installed: *)
     1.8 +(* requires a proof-generating SAT solver (zChaff or MiniSAT) to be *)
     1.9 +(* installed:                                                       *)
    1.10  try time_use_thy "SAT_Examples";
    1.11  
    1.12 -(* requires zChaff (or some other reasonably fast SAT solver) to be installed: *)
    1.13 +(* requires zChaff (or some other reasonably fast SAT solver) to be *)
    1.14 +(* installed:                                                       *)
    1.15  if getenv "ZCHAFF_HOME" <> "" then
    1.16    time_use_thy "Sudoku"
    1.17 -else
    1.18 -  ();
    1.19 +else ();
    1.20  
    1.21  time_use_thy "Refute_Examples";
    1.22  time_use_thy "Quickcheck_Examples";