small fixes in docs

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

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

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