| changeset 32518 | e3c4e337196c |
| parent 32496 | 4ab00a2642c3 |
| child 32564 | 378528d2f7eb |
| 32517:bfe7573a239b | 32518:e3c4e337196c |
|---|---|
1 (* Title: Mirabelle_Test.thy |
|
2 Author: Sascha Boehme |
|
3 *) |
|
4 |
|
5 header {* Simple test theory for Mirabelle actions *} |
|
6 |
|
7 theory Mirabelle_Test |
|
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 |