--- a/src/HOL/ex/SAT_Examples.thy Fri Jul 07 15:13:15 2006 +0200
+++ b/src/HOL/ex/SAT_Examples.thy Fri Jul 07 18:13:58 2006 +0200
@@ -10,6 +10,7 @@
begin
+(* ML {* sat.solver := "zchaff_with_proofs"; *} *)
ML {* set sat.trace_sat; *}
ML {* set quick_and_dirty; *}