src/HOL/ATP.thy
changeset 48891 c0eafbd55de3
parent 47946 33afcfad3f8d
child 51575 907efc894051
     1.1 --- a/src/HOL/ATP.thy	Wed Aug 22 22:47:16 2012 +0200
     1.2 +++ b/src/HOL/ATP.thy	Wed Aug 22 22:55:41 2012 +0200
     1.3 @@ -7,17 +7,15 @@
     1.4  
     1.5  theory ATP
     1.6  imports Meson
     1.7 -uses "Tools/lambda_lifting.ML"
     1.8 -     "Tools/monomorph.ML"
     1.9 -     "Tools/ATP/atp_util.ML"
    1.10 -     "Tools/ATP/atp_problem.ML"
    1.11 -     "Tools/ATP/atp_proof.ML"
    1.12 -     "Tools/ATP/atp_proof_redirect.ML"
    1.13 -     ("Tools/ATP/atp_problem_generate.ML")
    1.14 -     ("Tools/ATP/atp_proof_reconstruct.ML")
    1.15 -     ("Tools/ATP/atp_systems.ML")
    1.16  begin
    1.17  
    1.18 +ML_file "Tools/lambda_lifting.ML"
    1.19 +ML_file "Tools/monomorph.ML"
    1.20 +ML_file "Tools/ATP/atp_util.ML"
    1.21 +ML_file "Tools/ATP/atp_problem.ML"
    1.22 +ML_file "Tools/ATP/atp_proof.ML"
    1.23 +ML_file "Tools/ATP/atp_proof_redirect.ML"
    1.24 +
    1.25  subsection {* Higher-order reasoning helpers *}
    1.26  
    1.27  definition fFalse :: bool where [no_atp]:
    1.28 @@ -132,9 +130,9 @@
    1.29  
    1.30  subsection {* Setup *}
    1.31  
    1.32 -use "Tools/ATP/atp_problem_generate.ML"
    1.33 -use "Tools/ATP/atp_proof_reconstruct.ML"
    1.34 -use "Tools/ATP/atp_systems.ML"
    1.35 +ML_file "Tools/ATP/atp_problem_generate.ML"
    1.36 +ML_file "Tools/ATP/atp_proof_reconstruct.ML"
    1.37 +ML_file "Tools/ATP/atp_systems.ML"
    1.38  
    1.39  setup ATP_Systems.setup
    1.40