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"
```