src/HOL/Metis.thy
changeset 48891 c0eafbd55de3
parent 47946 33afcfad3f8d
child 52641 c56b6fa636e8
     1.1 --- a/src/HOL/Metis.thy	Wed Aug 22 22:47:16 2012 +0200
     1.2 +++ b/src/HOL/Metis.thy	Wed Aug 22 22:55:41 2012 +0200
     1.3 @@ -9,13 +9,10 @@
     1.4  theory Metis
     1.5  imports ATP
     1.6  keywords "try0" :: diag
     1.7 -uses "~~/src/Tools/Metis/metis.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/try0.ML")
    1.12  begin
    1.13  
    1.14 +ML_file "~~/src/Tools/Metis/metis.ML"
    1.15 +
    1.16  subsection {* Literal selection and lambda-lifting helpers *}
    1.17  
    1.18  definition select :: "'a \<Rightarrow> 'a" where
    1.19 @@ -41,9 +38,9 @@
    1.20  
    1.21  subsection {* Metis package *}
    1.22  
    1.23 -use "Tools/Metis/metis_generate.ML"
    1.24 -use "Tools/Metis/metis_reconstruct.ML"
    1.25 -use "Tools/Metis/metis_tactic.ML"
    1.26 +ML_file "Tools/Metis/metis_generate.ML"
    1.27 +ML_file "Tools/Metis/metis_reconstruct.ML"
    1.28 +ML_file "Tools/Metis/metis_tactic.ML"
    1.29  
    1.30  setup {* Metis_Tactic.setup *}
    1.31  
    1.32 @@ -58,8 +55,7 @@
    1.33  
    1.34  subsection {* Try0 *}
    1.35  
    1.36 -use "Tools/try0.ML"
    1.37 -
    1.38 +ML_file "Tools/try0.ML"
    1.39  setup {* Try0.setup *}
    1.40  
    1.41  end