equal
deleted
inserted
replaced
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 |
9 uses |
10 "Actions/mirabelle_arith.ML" |
10 "Tools/mirabelle_arith.ML" |
11 "Actions/mirabelle_metis.ML" |
11 "Tools/mirabelle_metis.ML" |
12 "Actions/mirabelle_quickcheck.ML" |
12 "Tools/mirabelle_quickcheck.ML" |
13 "Actions/mirabelle_refute.ML" |
13 "Tools/mirabelle_refute.ML" |
14 "Actions/mirabelle_sledgehammer.ML" |
14 "Tools/mirabelle_sledgehammer.ML" |
15 "Actions/mirabelle_sledgehammer_filter.ML" |
15 "Tools/mirabelle_sledgehammer_filter.ML" |
16 begin |
16 begin |
17 |
17 |
18 text {* |
18 text {* |
19 Only perform type-checking of the actions, |
19 Only perform type-checking of the actions, |
20 any reasonable test would be too complicated. |
20 any reasonable test would be too complicated. |