src/HOL/ex/SAT_Examples.thy

 shows "False"
 using assms
 (*
 by sat
 *)
-by rawsat  -- \<open>this is without CNF conversion\<close>
+by rawsat  \<comment> \<open>this is without CNF conversion\<close>
 
 (* Translated from TPTP problem library: MSC007-1.008.dimacs *)
 
 lemma assumes 1: "x0 | x1 | x2 | x3 | x4 | x5 | x6"
 and 2: "x7 | x8 | x9 | x10 | x11 | x12 | x13"

 shows "False"
 using assms
 (*
 by sat
 *)
-by rawsat  -- \<open>this is without CNF conversion\<close>
+by rawsat  \<comment> \<open>this is without CNF conversion\<close>
 
 (* 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
    sat, minisat_with_proofs: 40790 resolution steps in