--- a/src/HOL/Mirabelle.thy Sun Jun 06 21:39:26 2021 +0200
+++ b/src/HOL/Mirabelle.thy Thu Jun 10 11:21:57 2021 +0200
@@ -1,6 +1,8 @@
(* Title: HOL/Mirabelle.thy
- Author: Jasmin Blanchette and Sascha Boehme, TU Munich
+ Author: Jasmin Blanchette, TU Munich
+ Author: Sascha Boehme, TU Munich
Author: Makarius
+ Author: Martin Desharnais, UniBw Munich
*)
theory Mirabelle
@@ -8,6 +10,13 @@
begin
ML_file \<open>Tools/Mirabelle/mirabelle.ML\<close>
+
+ML \<open>
+signature MIRABELLE_ACTION = sig
+ val make_action : Mirabelle.action_context -> Mirabelle.action
+end
+\<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>
@@ -15,4 +24,4 @@
ML_file \<open>Tools/Mirabelle/mirabelle_sledgehammer_filter.ML\<close>
ML_file \<open>Tools/Mirabelle/mirabelle_try0.ML\<close>
-end
+end
\ No newline at end of file