equal
deleted
inserted
replaced
4 |
4 |
5 header {* Simple test theory for Mirabelle actions *} |
5 header {* Simple test theory for Mirabelle actions *} |
6 |
6 |
7 theory Mirabelle_Test |
7 theory Mirabelle_Test |
8 imports Main Mirabelle |
8 imports Main Mirabelle |
9 uses |
|
10 "Tools/mirabelle_arith.ML" |
|
11 "Tools/mirabelle_metis.ML" |
|
12 "Tools/mirabelle_quickcheck.ML" |
|
13 "Tools/mirabelle_refute.ML" |
|
14 "Tools/mirabelle_sledgehammer.ML" |
|
15 "Tools/mirabelle_sledgehammer_filter.ML" |
|
16 "Tools/mirabelle_try0.ML" |
|
17 begin |
9 begin |
|
10 |
|
11 ML_file "Tools/mirabelle_arith.ML" |
|
12 ML_file "Tools/mirabelle_metis.ML" |
|
13 ML_file "Tools/mirabelle_quickcheck.ML" |
|
14 ML_file "Tools/mirabelle_refute.ML" |
|
15 ML_file "Tools/mirabelle_sledgehammer.ML" |
|
16 ML_file "Tools/mirabelle_sledgehammer_filter.ML" |
|
17 ML_file "Tools/mirabelle_try0.ML" |
18 |
18 |
19 text {* |
19 text {* |
20 Only perform type-checking of the actions, |
20 Only perform type-checking of the actions, |
21 any reasonable test would be too complicated. |
21 any reasonable test would be too complicated. |
22 *} |
22 *} |