diff --git a/docs/index.html b/docs/index.html
index 2d84382..e26deff 100644
--- a/docs/index.html
+++ b/docs/index.html
@@ -223,13 +223,14 @@ <h2 id="compiling-and-running-benchmarks">Compiling and running benchmarks</h2>
 ./bench_kmp.sh -r
 cd sorting
 make run</code></pre>
-<p>This will run the binary search, KMP, and parallel sorting benchmarks. Warning: We have only tested this on a Linux x86_64 platform so far. We do not (yet) know how LLVM will digest our code on other platforms.</p>
+<p>This will run the binary search, KMP, and parallel sorting benchmarks. In order to run the Imperative HOL benchmarks for bs and KMP, an MLton compiler is required. Warning: We have only tested this on a Linux x86_64 platform so far. We do not (yet) know how LLVM will digest our code on other platforms.</p>
 <p>To render the sorting benchmark results as pdf file, type (still in sorting directory):</p>
 <pre><code>make report</code></pre>
+<p>This requires pdflatex with the pgfplots package.</p>
 <h2 id="re-checking-the-proofs">Re-Checking the Proofs</h2>
 <p>To re-check the proofs, run</p>
 <pre><code>  cd thys 
-  isabelle build -D.</code></pre>
+  isabelle build -b -D.</code></pre>
 <p>Here, <code>isabelle</code> must refer to <code>/your/path/to/Isabelle2022/bin/isabelle</code> from your Isabelle installation. This will invoke Isabelle to check all proofs and re-generate the exported code.</p>
 <h3 id="regression-test-script">Regression Test Script</h3>
 <p>To run a quick regression test script</p>
diff --git a/docs/index.md b/docs/index.md
index 61608e6..fd8705d 100644
--- a/docs/index.md
+++ b/docs/index.md
@@ -112,6 +112,7 @@ The main features are:
     make run
 
   This will run the binary search, KMP, and parallel sorting benchmarks.
+  In order to run the Imperative HOL benchmarks for bs and KMP, an MLton compiler is required.
   Warning: We have only tested this on a Linux x86_64 platform so far. 
   We do not (yet) know how LLVM will digest our code on other platforms.
 
@@ -119,12 +120,14 @@ The main features are:
 
     make report
 
+  This requires pdflatex with the pgfplots package.
+
 
 ## Re-Checking the Proofs
   To re-check the proofs, run
 
       cd thys 
-      isabelle build -D.
+      isabelle build -b -D.
 
   Here, <code>isabelle</code> must refer to <code>/your/path/to/Isabelle2022/bin/isabelle</code> from your Isabelle installation.
   This will invoke Isabelle to check all proofs and re-generate the exported code.
diff --git a/index.in.md b/index.in.md
index 07647c8..1ba173e 100644
--- a/index.in.md
+++ b/index.in.md
@@ -112,6 +112,7 @@ The main features are:
     make run
 
   This will run the binary search, KMP, and parallel sorting benchmarks.
+  In order to run the Imperative HOL benchmarks for bs and KMP, an MLton compiler is required.
   Warning: We have only tested this on a Linux x86_64 platform so far. 
   We do not (yet) know how LLVM will digest our code on other platforms.
 
@@ -119,12 +120,14 @@ The main features are:
 
     make report
 
+  This requires pdflatex with the pgfplots package.
+
 
 ## Re-Checking the Proofs
   To re-check the proofs, run
 
       cd thys 
-      isabelle build -D.
+      isabelle build -b -D.
 
   Here, <code>isabelle</code> must refer to <code>/your/path/to/Isabelle2022/bin/isabelle</code> from your Isabelle installation.
   This will invoke Isabelle to check all proofs and re-generate the exported code.
diff --git a/index.md b/index.md
index 61608e6..fd8705d 100644
--- a/index.md
+++ b/index.md
@@ -112,6 +112,7 @@ The main features are:
     make run
 
   This will run the binary search, KMP, and parallel sorting benchmarks.
+  In order to run the Imperative HOL benchmarks for bs and KMP, an MLton compiler is required.
   Warning: We have only tested this on a Linux x86_64 platform so far. 
   We do not (yet) know how LLVM will digest our code on other platforms.
 
@@ -119,12 +120,14 @@ The main features are:
 
     make report
 
+  This requires pdflatex with the pgfplots package.
+
 
 ## Re-Checking the Proofs
   To re-check the proofs, run
 
       cd thys 
-      isabelle build -D.
+      isabelle build -b -D.
 
   Here, <code>isabelle</code> must refer to <code>/your/path/to/Isabelle2022/bin/isabelle</code> from your Isabelle installation.
   This will invoke Isabelle to check all proofs and re-generate the exported code.