src/HOL/ATP.thy
changeset 60758 d8d85a8172b5
parent 58889 5b7a9633cfa8
child 66364 fa3247e6ee4b
     1.1 --- a/src/HOL/ATP.thy	Sat Jul 18 21:44:18 2015 +0200
     1.2 +++ b/src/HOL/ATP.thy	Sat Jul 18 22:58:50 2015 +0200
     1.3 @@ -3,13 +3,13 @@
     1.4      Author:     Jasmin Blanchette, TU Muenchen
     1.5  *)
     1.6  
     1.7 -section {* Automatic Theorem Provers (ATPs) *}
     1.8 +section \<open>Automatic Theorem Provers (ATPs)\<close>
     1.9  
    1.10  theory ATP
    1.11  imports Meson
    1.12  begin
    1.13  
    1.14 -subsection {* ATP problems and proofs *}
    1.15 +subsection \<open>ATP problems and proofs\<close>
    1.16  
    1.17  ML_file "Tools/ATP/atp_util.ML"
    1.18  ML_file "Tools/ATP/atp_problem.ML"
    1.19 @@ -18,7 +18,7 @@
    1.20  ML_file "Tools/ATP/atp_satallax.ML"
    1.21  
    1.22  
    1.23 -subsection {* Higher-order reasoning helpers *}
    1.24 +subsection \<open>Higher-order reasoning helpers\<close>
    1.25  
    1.26  definition fFalse :: bool where
    1.27  "fFalse \<longleftrightarrow> False"
    1.28 @@ -131,7 +131,7 @@
    1.29  unfolding fFalse_def fTrue_def fequal_def by auto
    1.30  
    1.31  
    1.32 -subsection {* Waldmeister helpers *}
    1.33 +subsection \<open>Waldmeister helpers\<close>
    1.34  
    1.35  (* Has all needed simplification lemmas for logic. *)
    1.36  lemma boolean_equality: "(P \<longleftrightarrow> P) = True"
    1.37 @@ -144,7 +144,7 @@
    1.38    simp_thms(1-5,7-8,11-25,27-33) disj_comms disj_assoc conj_comms conj_assoc
    1.39  
    1.40  
    1.41 -subsection {* Basic connection between ATPs and HOL *}
    1.42 +subsection \<open>Basic connection between ATPs and HOL\<close>
    1.43  
    1.44  ML_file "Tools/lambda_lifting.ML"
    1.45  ML_file "Tools/monomorph.ML"