src/HOL/Library/Refute.thy
changeset 60500 903bb1495239
parent 58881 b9556a055632
child 63432 ba7901e94e7b
     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