src/HOL/Metis.thy
changeset 46320 0b8b73b49848
parent 45511 9b0f8ca4388e
child 46641 8801a24f9e9a
     1.1 --- a/src/HOL/Metis.thy	Mon Jan 23 17:40:31 2012 +0100
     1.2 +++ b/src/HOL/Metis.thy	Mon Jan 23 17:40:32 2012 +0100
     1.3 @@ -9,7 +9,7 @@
     1.4  theory Metis
     1.5  imports ATP
     1.6  uses "~~/src/Tools/Metis/metis.ML"
     1.7 -     ("Tools/Metis/metis_translate.ML")
     1.8 +     ("Tools/Metis/metis_generate.ML")
     1.9       ("Tools/Metis/metis_reconstruct.ML")
    1.10       ("Tools/Metis/metis_tactic.ML")
    1.11       ("Tools/try_methods.ML")
    1.12 @@ -40,7 +40,7 @@
    1.13  
    1.14  subsection {* Metis package *}
    1.15  
    1.16 -use "Tools/Metis/metis_translate.ML"
    1.17 +use "Tools/Metis/metis_generate.ML"
    1.18  use "Tools/Metis/metis_reconstruct.ML"
    1.19  use "Tools/Metis/metis_tactic.ML"
    1.20