equal
deleted
inserted
replaced
1 (* Title: HOL/Mirabelle/Mirabelle_Test.thy |
|
2 Author: Sascha Boehme, TU Munich |
|
3 *) |
|
4 |
|
5 section \<open>Simple test theory for Mirabelle actions\<close> |
|
6 |
|
7 theory Mirabelle_Test |
|
8 imports Main Mirabelle |
|
9 begin |
|
10 |
|
11 ML_file \<open>Tools/mirabelle_arith.ML\<close> |
|
12 ML_file \<open>Tools/mirabelle_metis.ML\<close> |
|
13 ML_file \<open>Tools/mirabelle_quickcheck.ML\<close> |
|
14 ML_file \<open>Tools/mirabelle_sledgehammer.ML\<close> |
|
15 ML_file \<open>Tools/mirabelle_sledgehammer_filter.ML\<close> |
|
16 ML_file \<open>Tools/mirabelle_try0.ML\<close> |
|
17 |
|
18 text \<open> |
|
19 Only perform type-checking of the actions, |
|
20 any reasonable test would be too complicated. |
|
21 \<close> |
|
22 |
|
23 end |
|