diff -r 2e48182cc82c -r cf58b5b794b2 src/HOL/ex/SAT_Examples.thy
--- a/src/HOL/ex/SAT_Examples.thy	Sat Dec 26 15:44:14 2015 +0100
+++ b/src/HOL/ex/SAT_Examples.thy	Sat Dec 26 15:59:27 2015 +0100
@@ -277,7 +277,7 @@
 (*
 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 *)
 
@@ -490,7 +490,7 @@
 (*
 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