|
32564
|
1 |
(* Title: HOL/Mirabelle/Mirabelle_Test.thy
|
|
|
2 |
Author: Sascha Boehme, TU Munich
|
|
32496
|
3 |
*)
|
|
|
4 |
|
|
|
5 |
header {* Simple test theory for Mirabelle actions *}
|
|
|
6 |
|
|
32518
|
7 |
theory Mirabelle_Test
|
|
32496
|
8 |
imports Main Mirabelle
|
|
|
9 |
begin
|
|
|
10 |
|
|
48891
|
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 |
|
|
32564
|
19 |
text {*
|
|
|
20 |
Only perform type-checking of the actions,
|
|
|
21 |
any reasonable test would be too complicated.
|
|
|
22 |
*}
|
|
32496
|
23 |
|
|
|
24 |
end
|