--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mirabelle.thy Fri May 14 21:32:11 2021 +0200
@@ -0,0 +1,19 @@
+(* Title: HOL/Mirabelle.thy
+ Author: Jasmin Blanchette and Sascha Boehme, TU Munich
+*)
+
+theory Mirabelle
+ imports Sledgehammer Predicate_Compile
+begin
+
+ML_file \<open>Tools/Mirabelle/mirabelle.ML\<close>
+ML_file \<open>Tools/Mirabelle/mirabelle_arith.ML\<close>
+ML_file \<open>Tools/Mirabelle/mirabelle_metis.ML\<close>
+ML_file \<open>Tools/Mirabelle/mirabelle_quickcheck.ML\<close>
+(*
+ML_file \<open>Tools/Mirabelle/mirabelle_sledgehammer.ML\<close>
+ML_file \<open>Tools/Mirabelle/mirabelle_sledgehammer_filter.ML\<close>
+*)
+ML_file \<open>Tools/Mirabelle/mirabelle_try0.ML\<close>
+
+end