src/HOL/Mirabelle/Mirabelle_Test.thy
changeset 48891 c0eafbd55de3
parent 47891 e3627a83b114
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Mirabelle/Mirabelle_Test.thy	Wed Aug 22 22:47:16 2012 +0200
     1.2 +++ b/src/HOL/Mirabelle/Mirabelle_Test.thy	Wed Aug 22 22:55:41 2012 +0200
     1.3 @@ -6,16 +6,16 @@
     1.4  
     1.5  theory Mirabelle_Test
     1.6  imports Main Mirabelle
     1.7 -uses
     1.8 -  "Tools/mirabelle_arith.ML"
     1.9 -  "Tools/mirabelle_metis.ML"
    1.10 -  "Tools/mirabelle_quickcheck.ML"
    1.11 -  "Tools/mirabelle_refute.ML"
    1.12 -  "Tools/mirabelle_sledgehammer.ML"
    1.13 -  "Tools/mirabelle_sledgehammer_filter.ML"
    1.14 -  "Tools/mirabelle_try0.ML"
    1.15  begin
    1.16  
    1.17 +ML_file "Tools/mirabelle_arith.ML"
    1.18 +ML_file "Tools/mirabelle_metis.ML"
    1.19 +ML_file "Tools/mirabelle_quickcheck.ML"
    1.20 +ML_file "Tools/mirabelle_refute.ML"
    1.21 +ML_file "Tools/mirabelle_sledgehammer.ML"
    1.22 +ML_file "Tools/mirabelle_sledgehammer_filter.ML"
    1.23 +ML_file "Tools/mirabelle_try0.ML"
    1.24 +
    1.25  text {*
    1.26    Only perform type-checking of the actions,
    1.27    any reasonable test would be too complicated.