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