# HG changeset patch
# User webertj
# Date 1168453109 -3600
# Node ID 4cb2fe751952419e1c0c06d192833e3f67184ac8
# Parent  4b713f89f8c743f037ba7d3ae08f54f3da3ebee9
minor comment change

diff -r 4b713f89f8c7 -r 4cb2fe751952 src/HOL/ex/SAT_Examples.thy
--- 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