diff --git a/docs/src/knuthbendix1.md b/docs/src/knuthbendix1.md
index 697ee5d0..d3de39d4 100644
--- a/docs/src/knuthbendix1.md
+++ b/docs/src/knuthbendix1.md
@@ -61,10 +61,11 @@ reduce!(::KBS1AlgPlain, ::RewritingSystem)
 [^Sims1994]: Charles C. Sims _Computation with finitely presented groups_,
              Cambridge University Press, 1994.
 
-## Example from the theoretical section
+## Example from theoretical section
 
-To reproduce computations of the [Example](@ref) one could call `knuthbendix1`
-as follows.
+To reproduce the computations of the
+[Example](@ref "Knuth Bendix completion - an example") one could call
+`knuthbendix1` with `verbosity=2` which prints step-by-step information.
 
 ```@meta
 CurrentModule = KnuthBendix
diff --git a/docs/src/knuthbendix2.md b/docs/src/knuthbendix2.md
index a09b4fc8..e8426a9b 100644
--- a/docs/src/knuthbendix2.md
+++ b/docs/src/knuthbendix2.md
@@ -1,6 +1,6 @@
 # Using a stack
 
-As can be observed in [Knuth Bendix completion -- an example](@ref) after we
+As can be observed in [Knuth Bendix completion - an example](@ref) after we
 have added rule 6, there was no point considering rule 5, since it was
 rendered redundant. This can be achieved by keeping a boolean variable for each
 rule indicating its status, and flipping it to `false` when it becomes
diff --git a/docs/src/knuthbendix_completion.md b/docs/src/knuthbendix_completion.md
index 960aff1e..9452c53d 100644
--- a/docs/src/knuthbendix_completion.md
+++ b/docs/src/knuthbendix_completion.md
@@ -64,7 +64,7 @@ new rewriting rules are often discovered and added to $\mathcal{R}$ hence new
 additional pairs of rules need to be checked and the whole process becomes
 potentially infinite.
 
-## Knuth Bendix completion -- an example
+## Knuth Bendix completion - an example
 
 Let us work out an example. We begin with alphabet $\mathcal{A} = \{a, A, b\}$
 ordered by the length-then-lexicographical order on $\mathcal{A}^*$ defined by