src/HOL/Metis.thy
changeset 60758 d8d85a8172b5
parent 58889 5b7a9633cfa8
child 62672 068b430e678f
     1.1 --- a/src/HOL/Metis.thy	Sat Jul 18 21:44:18 2015 +0200
     1.2 +++ b/src/HOL/Metis.thy	Sat Jul 18 22:58:50 2015 +0200
     1.3 @@ -4,7 +4,7 @@
     1.4      Author:     Jasmin Blanchette, TU Muenchen
     1.5  *)
     1.6  
     1.7 -section {* Metis Proof Method *}
     1.8 +section \<open>Metis Proof Method\<close>
     1.9  
    1.10  theory Metis
    1.11  imports ATP
    1.12 @@ -15,7 +15,7 @@
    1.13  declare [[ML_print_depth = 10]]
    1.14  
    1.15  
    1.16 -subsection {* Literal selection and lambda-lifting helpers *}
    1.17 +subsection \<open>Literal selection and lambda-lifting helpers\<close>
    1.18  
    1.19  definition select :: "'a \<Rightarrow> 'a" where
    1.20  "select = (\<lambda>x. x)"
    1.21 @@ -38,7 +38,7 @@
    1.22  unfolding lambda_def by assumption
    1.23  
    1.24  
    1.25 -subsection {* Metis package *}
    1.26 +subsection \<open>Metis package\<close>
    1.27  
    1.28  ML_file "Tools/Metis/metis_generate.ML"
    1.29  ML_file "Tools/Metis/metis_reconstruct.ML"