src/HOL/Metis.thy
changeset 46950 d0181abdbdac
parent 46641 8801a24f9e9a
child 47946 33afcfad3f8d
equal deleted inserted replaced
46949:94aa7b81bcf6 46950:d0181abdbdac
     6 
     6 
     7 header {* Metis Proof Method *}
     7 header {* Metis Proof Method *}
     8 
     8 
     9 theory Metis
     9 theory Metis
    10 imports ATP
    10 imports ATP
       
    11 keywords "try0" :: diag
    11 uses "~~/src/Tools/Metis/metis.ML"
    12 uses "~~/src/Tools/Metis/metis.ML"
    12      ("Tools/Metis/metis_generate.ML")
    13      ("Tools/Metis/metis_generate.ML")
    13      ("Tools/Metis/metis_reconstruct.ML")
    14      ("Tools/Metis/metis_reconstruct.ML")
    14      ("Tools/Metis/metis_tactic.ML")
    15      ("Tools/Metis/metis_tactic.ML")
    15      ("Tools/try0.ML")
    16      ("Tools/try0.ML")