| changeset 32496 | 4ab00a2642c3 |
| 32495:6decc1ffdbed | 32496:4ab00a2642c3 |
|---|---|
1 (* Title: MirabelleTest.thy |
|
2 Author: Sascha Boehme |
|
3 *) |
|
4 |
|
5 header {* Simple test theory for Mirabelle actions *} |
|
6 |
|
7 theory MirabelleTest |
|
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 begin |
|
16 |
|
17 (* |
|
18 only perform type-checking of the actions, |
|
19 any reasonable test would be too complicated |
|
20 *) |
|
21 |
|
22 end |