diff --git a/docs/source/index.rst b/docs/source/index.rst
index 7e8948b..43c8185 100644
--- a/docs/source/index.rst
+++ b/docs/source/index.rst
@@ -10,11 +10,6 @@ formal tasks:
    * Unbounded verification of safety properties
    * Generation of test benches from cover statements
    * Verification of liveness properties
-   * Formal equivalence checking [TBD]
-   * Reactive Synthesis [TBD]
-
-(Items marked [TBD] are features under construction and not available
-at the moment.)
 
 .. toctree::
    :maxdepth: 3
diff --git a/docs/source/install.rst b/docs/source/install.rst
index a232c86..604737b 100644
--- a/docs/source/install.rst
+++ b/docs/source/install.rst
@@ -88,6 +88,7 @@ Boolector
 https://boolector.github.io
 
 .. code-block:: text
+    
     git clone https://github.com/boolector/boolector
     cd boolector
     ./contrib/setup-btor2tools.sh
diff --git a/docs/source/newstart.rst b/docs/source/newstart.rst
index 6b4c1ef..604d04c 100644
--- a/docs/source/newstart.rst
+++ b/docs/source/newstart.rst
@@ -233,7 +233,7 @@ while still passing all of the tests?
 .. note::
 
     If you need a **hint**, try increasing the width of the address wires.  4 bits
-    supports up to :math:`2^4=16` addresses.  Are there other signals that 
+    supports up to 2\ :sup:`4`\ =16 addresses.  Are there other signals that 
     need to be wider?  Can you make the width parameterisable to support 
     arbitrarily large buffers?