diff --git a/data/CHANGES b/data/CHANGES
--- a/data/CHANGES
+++ b/data/CHANGES
@@ -1,3 +1,7 @@
+* 0.8.6.0
+  - Incorporate a patch contributed by Ognjen Maric that improves reasoning
+    about injective facts in inductive proofs.
+
 * 0.8.5.1
   - Added KEA+ models with adversarial key registration.
   - Make case splitting more extensive. This possibly increases precomputation
diff --git a/tamarin-prover.cabal b/tamarin-prover.cabal
--- a/tamarin-prover.cabal
+++ b/tamarin-prover.cabal
@@ -1,7 +1,7 @@
 cabal-version:      >= 1.8
 build-type:         Simple
 name:               tamarin-prover
-version:            0.8.5.1
+version:            0.8.6.0
 license:            GPL
 license-file:       LICENSE
 category:           Theorem Provers
@@ -273,7 +273,7 @@
 
       , tamarin-prover-utils  >= 0.8.5.1  && < 0.9
       , tamarin-prover-term   >= 0.8.5.1  && < 0.9
-      , tamarin-prover-theory >= 0.8.5.1  && < 0.9
+      , tamarin-prover-theory >= 0.8.6.0  && < 0.9
 
 
     other-modules: