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