# HG changeset patch
# User webertj
# Date 1180722852 -7200
# Node ID b7f3a30f3d7f9e8571f1a0d6cdbf11f2d188aeaa
# Parent  d45c4d6c5f15f8416092cf2e97d9b26dfe97c239
MiniSAT mentioned in comment

diff -r d45c4d6c5f15 -r b7f3a30f3d7f src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Fri Jun 01 16:04:13 2007 +0200
+++ b/src/HOL/ex/ROOT.ML	Fri Jun 01 20:34:12 2007 +0200
@@ -61,14 +61,15 @@
 time_use_thy "SVC_Oracle";
 if_svc_enabled time_use_thy "svc_test";
 
-(* requires zChaff with proof generation to be installed: *)
+(* requires a proof-generating SAT solver (zChaff or MiniSAT) to be *)
+(* installed:                                                       *)
 try time_use_thy "SAT_Examples";
 
-(* requires zChaff (or some other reasonably fast SAT solver) to be installed: *)
+(* requires zChaff (or some other reasonably fast SAT solver) to be *)
+(* installed:                                                       *)
 if getenv "ZCHAFF_HOME" <> "" then
   time_use_thy "Sudoku"
-else
-  ();
+else ();
 
 time_use_thy "Refute_Examples";
 time_use_thy "Quickcheck_Examples";