diff --git a/src/HOL/Mirabelle.thy b/src/HOL/Mirabelle.thy
--- a/src/HOL/Mirabelle.thy
+++ b/src/HOL/Mirabelle.thy
@@ -1,27 +1,28 @@
 (*  Title:      HOL/Mirabelle.thy
     Author:     Jasmin Blanchette, TU Munich
     Author:     Sascha Boehme, TU Munich
     Author:     Makarius
-    Author:     Martin Desharnais, UniBw Munich
+    Author:     Martin Desharnais, UniBw Munich, MPI-INF Saarbrücken
 *)
 
 theory Mirabelle
-  imports Sledgehammer Predicate_Compile
+  imports Sledgehammer Predicate_Compile Presburger
 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_presburger.ML\<close>
 ML_file \<open>Tools/Mirabelle/mirabelle_quickcheck.ML\<close>
+ML_file \<open>Tools/Mirabelle/mirabelle_sledgehammer_filter.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
\ No newline at end of file
+end
diff --git a/src/HOL/Tools/Mirabelle/mirabelle_presburger.ML b/src/HOL/Tools/Mirabelle/mirabelle_presburger.ML
new file mode 100644
--- /dev/null
+++ b/src/HOL/Tools/Mirabelle/mirabelle_presburger.ML
@@ -0,0 +1,21 @@
+(*  Title:      HOL/Mirabelle/Tools/mirabelle_presburger.ML
+    Author:     Martin Desharnais, MPI-INF Saarbrücken
+
+Mirabelle action: "presburger".
+*)
+
+structure Mirabelle_Presburger: MIRABELLE_ACTION =
+struct
+
+fun make_action ({timeout, ...} : Mirabelle.action_context) =
+  let
+    val _ = Timing.timing
+    fun run_action ({pre, ...} : Mirabelle.command) =
+      (case Timing.timing (Mirabelle.can_apply timeout (Cooper.tac true [] [])) pre of
+        ({cpu, ...}, true) => "succeeded (" ^ Time.toString cpu ^ " s)"
+      | (_, false) => "failed")
+  in {run_action = run_action, finalize = K ""} end
+
+val () = Mirabelle.register_action "presburger" make_action
+
+end