diff --git a/Manual/Cheatsheet/cheatsheet.css b/Manual/Cheatsheet/cheatsheet.css
index da29c8b16d..1b73b10ea9 100644
--- a/Manual/Cheatsheet/cheatsheet.css
+++ b/Manual/Cheatsheet/cheatsheet.css
@@ -31,7 +31,7 @@ h1, h2, h3 {
 
 h1 {
   font-size: 1.8rem;
-  margin-bottom: 30px;
+  margin: 30px 0;
 }
 
 h1, h2, h3, h4, h5, h6{
diff --git a/Manual/Cheatsheet/cheatsheet.md b/Manual/Cheatsheet/cheatsheet.md
index 7541e55236..a22c548195 100644
--- a/Manual/Cheatsheet/cheatsheet.md
+++ b/Manual/Cheatsheet/cheatsheet.md
@@ -496,7 +496,7 @@ In some cases, it is useful to generalise a goal in order to use a suitable indu
 <code>qspec_then &grave;<i>tm&grave; thm_tactic thm</i></code>
 : Instantiates the supplied (`∀`-quantified) theorem with the given term, and applies the theorem-tactic to the result.
 
-<code>qspecl_then [&grave;<i>tm&grave;s] thm_tactic thm</i></code>
+<code>qspecl_then [&grave;<i>tm</i>&grave;s] <i>thm_tactic thm</i></code>
 : Like `qspec_then`, but instantiates multiple `∀`-quantified variables.
 
 <code>imp_res_tac <i>theorem</i></code>