src/HOL/ATP.thy
changeset 43108 eb1e31eb7449
parent 43085 0a2f5b86bdd7
child 43678 56d352659500
equal deleted inserted replaced
43107:5792d6bb4fb1 43108:eb1e31eb7449
     5 
     5 
     6 header {* Automatic Theorem Provers (ATPs) *}
     6 header {* Automatic Theorem Provers (ATPs) *}
     7 
     7 
     8 theory ATP
     8 theory ATP
     9 imports Meson
     9 imports Meson
    10 uses "Tools/ATP/atp_util.ML"
    10 uses "Tools/monomorph.ML"
       
    11      "Tools/ATP/atp_util.ML"
    11      "Tools/ATP/atp_problem.ML"
    12      "Tools/ATP/atp_problem.ML"
    12      "Tools/ATP/atp_proof.ML"
    13      "Tools/ATP/atp_proof.ML"
    13      "Tools/ATP/atp_systems.ML"
    14      "Tools/ATP/atp_systems.ML"
    14      ("Tools/ATP/atp_translate.ML")
    15      ("Tools/ATP/atp_translate.ML")
    15      ("Tools/ATP/atp_reconstruct.ML")
    16      ("Tools/ATP/atp_reconstruct.ML")