--- a/src/HOL/Library/Refute.thy Wed Jun 17 10:57:11 2015 +0200
+++ b/src/HOL/Library/Refute.thy Wed Jun 17 11:03:05 2015 +0200
@@ -5,7 +5,7 @@
Basic setup and documentation for the 'refute' (and 'refute_params') command.
*)
-section {* Refute *}
+section \<open>Refute\<close>
theory Refute
imports Main
@@ -23,7 +23,7 @@
satsolver = auto,
no_assms = false]
-text {*
+text \<open>
\small
\begin{verbatim}
(* ------------------------------------------------------------------------- *)
@@ -107,6 +107,6 @@
(* HOL/ex/Refute_Examples.thy Examples *)
(* ------------------------------------------------------------------------- *)
\end{verbatim}
-*}
+\<close>
end