src/HOL/Mirabelle/Mirabelle_Test.thy
changeset 47477 3fabf352243e
parent 41358 d5e91925916e
child 47730 15f4309bb9eb
     1.1 --- a/src/HOL/Mirabelle/Mirabelle_Test.thy	Sat Apr 14 23:34:18 2012 +0200
     1.2 +++ b/src/HOL/Mirabelle/Mirabelle_Test.thy	Sat Apr 14 23:52:17 2012 +0100
     1.3 @@ -7,12 +7,12 @@
     1.4  theory Mirabelle_Test
     1.5  imports Main Mirabelle
     1.6  uses
     1.7 -  "Tools/mirabelle_arith.ML"
     1.8 -  "Tools/mirabelle_metis.ML"
     1.9 -  "Tools/mirabelle_quickcheck.ML"
    1.10 -  "Tools/mirabelle_refute.ML"
    1.11 -  "Tools/mirabelle_sledgehammer.ML"
    1.12 -  "Tools/mirabelle_sledgehammer_filter.ML"
    1.13 +  "Actions/mirabelle_arith.ML"
    1.14 +  "Actions/mirabelle_metis.ML"
    1.15 +  "Actions/mirabelle_quickcheck.ML"
    1.16 +  "Actions/mirabelle_refute.ML"
    1.17 +  "Actions/mirabelle_sledgehammer.ML"
    1.18 +  "Actions/mirabelle_sledgehammer_filter.ML"
    1.19  begin
    1.20  
    1.21  text {*