--- a/src/HOL/Tools/Mirabelle/mirabelle_arith.ML Sun Jun 06 21:39:26 2021 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle_arith.ML Thu Jun 10 11:21:57 2021 +0200
@@ -1,17 +1,24 @@
(* Title: HOL/Mirabelle/Tools/mirabelle_arith.ML
- 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
Mirabelle action: "arith".
*)
-structure Mirabelle_Arith: sig end =
+structure Mirabelle_Arith: MIRABELLE_ACTION =
struct
-val _ =
- Theory.setup (Mirabelle.command_action \<^binding>\<open>arith\<close>
- (fn {timeout, ...} => fn {pre, ...} =>
- if Mirabelle.can_apply timeout Arith_Data.arith_tac pre
- then "succeeded" else ""));
+fun make_action ({timeout, ...} : Mirabelle.action_context) =
+ let
+ fun run_action ({pre, ...} : Mirabelle.command) =
+ if Mirabelle.can_apply timeout Arith_Data.arith_tac pre then
+ "succeeded"
+ else
+ ""
+ in {run_action = run_action, finalize = K ""} end
+
+val () = Mirabelle.register_action "arith" make_action
end