--- a/src/HOL/ex/SAT_Examples.thy Wed Jan 10 19:17:52 2007 +0100
+++ b/src/HOL/ex/SAT_Examples.thy Wed Jan 10 19:18:29 2007 +0100
@@ -287,7 +287,7 @@
(*
by sat
*)
-by rawsat -- {* this is without CNF conversion time *}
+by rawsat -- {* this is without CNF conversion *}
(* Translated from TPTP problem library: MSC007-1.008.dimacs *)
@@ -510,7 +510,7 @@
(*
by sat
*)
-by rawsat -- {* this is without CNF conversion time *}
+by rawsat -- {* this is without CNF conversion *}
(* Old sequent clause representation ("[c_i, p, ~q, \<dots>] \<turnstile> False"):
sat, zchaff_with_proofs: 8705 resolution steps in +++ User 1.154 All 1.189 secs