1.1 --- a/src/HOL/Library/Refute.thy Wed Jun 17 10:57:11 2015 +0200
1.2 +++ b/src/HOL/Library/Refute.thy Wed Jun 17 11:03:05 2015 +0200
1.3 @@ -5,7 +5,7 @@
1.4 Basic setup and documentation for the 'refute' (and 'refute_params') command.
1.5 *)
1.6
1.7 -section {* Refute *}
1.8 +section \<open>Refute\<close>
1.9
1.10 theory Refute
1.11 imports Main
1.12 @@ -23,7 +23,7 @@
1.13 satsolver = auto,
1.14 no_assms = false]
1.15
1.16 -text {*
1.17 +text \<open>
1.18 \small
1.19 \begin{verbatim}
1.20 (* ------------------------------------------------------------------------- *)
1.21 @@ -107,6 +107,6 @@
1.22 (* HOL/ex/Refute_Examples.thy Examples *)
1.23 (* ------------------------------------------------------------------------- *)
1.24 \end{verbatim}
1.25 -*}
1.26 +\<close>
1.27
1.28 end