diff --git a/de.prob.eventb.disprover.core/plugin.xml b/de.prob.eventb.disprover.core/plugin.xml
index a6445540a17811179bb32fce4e74745e2374138c..30a8c2e72c6ef161759c1fdb7eb86fcece6f19d4 100644
--- a/de.prob.eventb.disprover.core/plugin.xml
+++ b/de.prob.eventb.disprover.core/plugin.xml
@@ -9,5 +9,14 @@
             name="%reasoner.name">
       </reasoner>
    </extension>
+   <extension
+         point="org.eventb.core.seqprover.autoTactics">
+      <autoTactic
+            class="de.prob.eventb.disprover.core.internal.DisproverAutoTactic"
+            description="%autotactic.desc"
+            id="disproverTactic"
+            name="%autotactic.name">
+      </autoTactic>
+   </extension>
 
 </plugin>
diff --git a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverAutoTactic.java b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverAutoTactic.java
new file mode 100644
index 0000000000000000000000000000000000000000..8c1e9db714adf73c65fcb0735005fcc6fc2d8a36
--- /dev/null
+++ b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverAutoTactic.java
@@ -0,0 +1,16 @@
+package de.prob.eventb.disprover.core.internal;
+
+import org.eventb.core.seqprover.ITactic;
+import org.eventb.core.seqprover.eventbExtensions.AutoTactics.AbsractLazilyConstrTactic;
+import org.eventb.core.seqprover.tactics.BasicTactics;
+
+import de.prob.eventb.disprover.core.DisproverReasonerInput;
+
+
+public class DisproverAutoTactic extends AbsractLazilyConstrTactic {
+	@Override
+	protected ITactic getSingInstance() {
+		return BasicTactics.reasonerTac(new DisproverReasoner(),
+				new DisproverReasonerInput());
+	}
+}
\ No newline at end of file