diff --git a/GlimpseOfLean/Exercises/01Rewriting.lean b/GlimpseOfLean/Exercises/01Rewriting.lean
index 2403c9c..507fded 100644
--- a/GlimpseOfLean/Exercises/01Rewriting.lean
+++ b/GlimpseOfLean/Exercises/01Rewriting.lean
@@ -31,8 +31,8 @@ example (a b : ℝ) : (a+b)^2 = a^2 + 2*a*b + b^2 := by {
 /- In the first example above, take a closer look at where Lean displays parentheses.
 The `ring` tactic certainly knows about associativity of multiplication, but sometimes
 it is useful to understand that binary operation really are binary and an expression like
-`a*b*c` is read as `(a*b)*c` by Lean and the fact that is equal `a*(b*c)` is a lemma
-that is used by the `ring` tactic when needed.
+`a*b*c` is read as `(a*b)*c` by Lean and the fact that this is equal to `a*(b*c)` is a
+lemma that is used by the `ring` tactic when needed.
 -/
 
 
@@ -84,8 +84,8 @@ In the previous examples, we rewrote the goal using a local assumption. But we c
 also use lemmas. For instance let us prove a lemma about exponentiation.
 Since `ring` only knows how to prove things from the axioms of rings,
 it doesn't know how to work with exponentiation.
-For the following lemma, we will rewrite with the lemma
-`exp_add x y` twice, which is a proof that `exp(x+y) = exp(x) * exp(y)`.
+For the following lemma, we will rewrite twice with the lemma
+`exp_add x y`, which is a proof that `exp(x+y) = exp(x) * exp(y)`.
 -/
 example (a b c : ℝ) : exp (a + b + c) = exp a * exp b * exp c := by {
   rw [exp_add (a + b) c]
diff --git a/GlimpseOfLean/Exercises/03Forall.lean b/GlimpseOfLean/Exercises/03Forall.lean
index 63ef818..c83e676 100644
--- a/GlimpseOfLean/Exercises/03Forall.lean
+++ b/GlimpseOfLean/Exercises/03Forall.lean
@@ -59,10 +59,9 @@ example (f g : ℝ → ℝ) (hf : even_fun f) (hg : even_fun g) : even_fun (f +
 Tactics like `unfold`, `apply`, `exact`, `rfl` and `calc` will automatically unfold definitions.
 You can test this by deleting the `unfold` lines in the above example.
 
-Tactics like `rw`, `ring` and `linarith` will generally
-not unfold definitions that appear in the goal.
+Tactics like `rw` and `ring` will generally not unfold definitions that appear in the goal.
 This is why the first computation line is necessary, although its proof is simply `rfl`.
-Before that line, `rw hf x` won't find anything like `f (-x)` hence will give up.
+Before that line, `rw [hf x]` won't find anything like `f (-x)` hence will give up.
 The last line is not necessary however, since it only proves
 something that is true by definition, and is not followed by a `rw`.
 
@@ -170,7 +169,7 @@ example (f g : ℝ → ℝ) (hf : non_decreasing f) (hg : non_increasing g) :
 /- # Finding lemmas
 
 Lean's mathematical library contains many useful facts,
-and remembering all of them my name is infeasible.
+and remembering all of them by name is infeasible.
 The following exercises teach you two such techniques.
 * `simp` will simplify complicated expressions.
 * `apply?` will find lemmas from the library.
@@ -200,7 +199,8 @@ You learned about tactics:
 You now have a choice what to do next. There is one more basic file `04Exists`
 about the existential quantifier and conjunctions. You can do that now,
 or dive directly in one of the specialized files.
-In the latter case, you should come back to `04Exists` if you get stuck on anything with `∃`/`∧`.
+In the latter case, you should come back to `04Exists` if you get stuck on anything with `∃`/`∧`
+(where `∧` is the symbol for conjunctions, aka the logical “and” operator).
 
 You can start with specialized files in the `Topics` folder. You have choice between
 * `ClassicalPropositionalLogic` (easier, logic) if you want to learn
diff --git a/GlimpseOfLean/Library/Basic.lean b/GlimpseOfLean/Library/Basic.lean
index ec66085..4b437d8 100644
--- a/GlimpseOfLean/Library/Basic.lean
+++ b/GlimpseOfLean/Library/Basic.lean
@@ -96,3 +96,13 @@ lemma lowerBounds_range {α ι : Type _} [Preorder α] {s : ι → α} {x : α}
 lemma upperBounds_range {α ι : Type _} [Preorder α] {s : ι → α} {x : α} :
     x ∈ upperBounds (Set.range s) ↔ ∀ i, s i ≤ x :=
   lowerBounds_range (α := OrderDual α)
+
+open Lean PrettyPrinter Delaborator
+
+@[delab app.Real.exp]
+def my : Delab := do
+  let args := (← SubExpr.getExpr).getAppArgs
+  let stx ← delab args[0]!
+  let e := mkIdent `exp
+  `(term|$e $stx)
+
diff --git a/GlimpseOfLean/Solutions/01Rewriting.lean b/GlimpseOfLean/Solutions/01Rewriting.lean
index 6300b42..2a79d6e 100644
--- a/GlimpseOfLean/Solutions/01Rewriting.lean
+++ b/GlimpseOfLean/Solutions/01Rewriting.lean
@@ -33,8 +33,8 @@ example (a b : ℝ) : (a+b)^2 = a^2 + 2*a*b + b^2 := by {
 /- In the first example above, take a closer look at where Lean displays parentheses.
 The `ring` tactic certainly knows about associativity of multiplication, but sometimes
 it is useful to understand that binary operation really are binary and an expression like
-`a*b*c` is read as `(a*b)*c` by Lean and the fact that is equal `a*(b*c)` is a lemma
-that is used by the `ring` tactic when needed.
+`a*b*c` is read as `(a*b)*c` by Lean and the fact that this is equal to `a*(b*c)` is a
+lemma that is used by the `ring` tactic when needed.
 -/
 
 
@@ -89,8 +89,8 @@ In the previous examples, we rewrote the goal using a local assumption. But we c
 also use lemmas. For instance let us prove a lemma about exponentiation.
 Since `ring` only knows how to prove things from the axioms of rings,
 it doesn't know how to work with exponentiation.
-For the following lemma, we will rewrite with the lemma
-`exp_add x y` twice, which is a proof that `exp(x+y) = exp(x) * exp(y)`.
+For the following lemma, we will rewrite twice with the lemma
+`exp_add x y`, which is a proof that `exp(x+y) = exp(x) * exp(y)`.
 -/
 example (a b c : ℝ) : exp (a + b + c) = exp a * exp b * exp c := by {
   rw [exp_add (a + b) c]
diff --git a/GlimpseOfLean/Solutions/03Forall.lean b/GlimpseOfLean/Solutions/03Forall.lean
index d1ef766..fc2c75b 100644
--- a/GlimpseOfLean/Solutions/03Forall.lean
+++ b/GlimpseOfLean/Solutions/03Forall.lean
@@ -59,10 +59,9 @@ example (f g : ℝ → ℝ) (hf : even_fun f) (hg : even_fun g) : even_fun (f +
 Tactics like `unfold`, `apply`, `exact`, `rfl` and `calc` will automatically unfold definitions.
 You can test this by deleting the `unfold` lines in the above example.
 
-Tactics like `rw`, `ring` and `linarith` will generally
-not unfold definitions that appear in the goal.
+Tactics like `rw` and `ring` will generally not unfold definitions that appear in the goal.
 This is why the first computation line is necessary, although its proof is simply `rfl`.
-Before that line, `rw hf x` won't find anything like `f (-x)` hence will give up.
+Before that line, `rw [hf x]` won't find anything like `f (-x)` hence will give up.
 The last line is not necessary however, since it only proves
 something that is true by definition, and is not followed by a `rw`.
 
@@ -179,7 +178,7 @@ example (f g : ℝ → ℝ) (hf : non_decreasing f) (hg : non_increasing g) :
 /- # Finding lemmas
 
 Lean's mathematical library contains many useful facts,
-and remembering all of them my name is infeasible.
+and remembering all of them by name is infeasible.
 The following exercises teach you two such techniques.
 * `simp` will simplify complicated expressions.
 * `apply?` will find lemmas from the library.
@@ -215,7 +214,8 @@ You learned about tactics:
 You now have a choice what to do next. There is one more basic file `04Exists`
 about the existential quantifier and conjunctions. You can do that now,
 or dive directly in one of the specialized files.
-In the latter case, you should come back to `04Exists` if you get stuck on anything with `∃`/`∧`.
+In the latter case, you should come back to `04Exists` if you get stuck on anything with `∃`/`∧`
+(where `∧` is the symbol for conjunctions, aka the logical “and” operator).
 
 You can start with specialized files in the `Topics` folder. You have choice between
 * `ClassicalPropositionalLogic` (easier, logic) if you want to learn