src/HOL/ATP.thy
changeset 57263 2b6a96cc64c9
parent 57262 b2c629647a14
child 57707 0242e9578828
     1.1 --- a/src/HOL/ATP.thy	Mon Jun 16 19:40:04 2014 +0200
     1.2 +++ b/src/HOL/ATP.thy	Mon Jun 16 19:40:59 2014 +0200
     1.3 @@ -9,8 +9,8 @@
     1.4  imports Meson
     1.5  begin
     1.6  
     1.7 -ML_file "Tools/lambda_lifting.ML"
     1.8 -ML_file "Tools/monomorph.ML"
     1.9 +subsection {* ATP problems and proofs *}
    1.10 +
    1.11  ML_file "Tools/ATP/atp_util.ML"
    1.12  ML_file "Tools/ATP/atp_problem.ML"
    1.13  ML_file "Tools/ATP/atp_proof.ML"
    1.14 @@ -137,8 +137,10 @@
    1.15    eq_ac disj_comms disj_assoc conj_comms conj_assoc
    1.16  
    1.17  
    1.18 -subsection {* Setup *}
    1.19 +subsection {* Basic connection between ATPs and HOL *}
    1.20  
    1.21 +ML_file "Tools/lambda_lifting.ML"
    1.22 +ML_file "Tools/monomorph.ML"
    1.23  ML_file "Tools/ATP/atp_problem_generate.ML"
    1.24  ML_file "Tools/ATP/atp_proof_reconstruct.ML"
    1.25  ML_file "Tools/ATP/atp_systems.ML"