diff --git a/data/CHANGES b/data/CHANGES
--- a/data/CHANGES
+++ b/data/CHANGES
@@ -1,3 +1,15 @@
+* 0.8.6.3
+  - Fix some formatting issues in the tamarin-prover.cabal description,
+    which were introduced in 0.8.6.2.
+
+* 0.8.6.2
+  - Change the package description because we now always recommend to build
+    tamarin-prover from source and not by downloading a package to hackage.
+    See the README on the development branch for installation instructions.
+
+* 0.8.6.1
+  - Tweak dependencies.
+
 * 0.8.6.0
   - Incorporate a patch contributed by Ognjen Maric that improves reasoning
     about injective facts in inductive proofs.
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.6.2
+version:            0.8.6.3
 license:            GPL
 license-file:       LICENSE
 category:           Theorem Provers
@@ -12,9 +12,10 @@
 synopsis:           The Tamarin prover for security protocol analysis.
 description:
 
-    **Note:** the tamarin-prover should be installed from source as described
-    in its README at <https://github.com/tamarin-prover/tamarin-prover>.
-
+    Note that the @tamarin-prover@ should be installed from source as
+    described in its README at
+    <https://github.com/tamarin-prover/tamarin-prover>.
+    .
     The Tamarin prover is a tool for the analysis of security protocols. It
     implements a constraint solving algorithm that supports both falsification
     and verification of security protocols with respect to an unbounded number
@@ -309,4 +310,3 @@
 source-repository head
   type:     git
   location: https://github.com/tamarin-prover/tamarin-prover.git
-