--- 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