diff --git a/04_Quantifiers_and_Equality.org b/04_Quantifiers_and_Equality.org
index 3c37eeb1..fc55f063 100644
--- a/04_Quantifiers_and_Equality.org
+++ b/04_Quantifiers_and_Equality.org
@@ -817,9 +817,9 @@ open nat algebra
 
 -- BEGIN
 variable f : ℕ → ℕ
-premise H : ∀ x : ℕ, f x ≤ f (x + 1)
 
-example (H' : ∃ x, f (x + 1) ≤ f x) : ∃ x, f (x + 1) = f x :=
+example (H : ∀ x : ℕ, f x ≤ f (x + 1)) (H' : ∃ x, f (x + 1) ≤ f x) :
+  ∃ x, f (x + 1) = f x :=
 obtain x `f (x + 1) ≤ f x`, from H',
 exists.intro x
   (show f (x + 1) = f x, from le.antisymm `f (x + 1) ≤ f x` (H x))
@@ -853,7 +853,7 @@ have even b,
 have 2 ∣ gcd a b,
   from dvd_gcd (dvd_of_even `even a`) (dvd_of_even `even b`),
 have 2 ∣ (1 : ℕ),
-  begin+ rewrite [gcd_eq_one_of_coprime co at this], exact this end,
+  by rewrite [gcd_eq_one_of_coprime co at this]; exact this,
 show false, from absurd `2 ∣ 1` dec_trivial
 #+END_SRC
 
diff --git a/08_Building_Theories_and_Proofs.org b/08_Building_Theories_and_Proofs.org
index 9387332d..72fdd6f5 100644
--- a/08_Building_Theories_and_Proofs.org
+++ b/08_Building_Theories_and_Proofs.org
@@ -828,64 +828,66 @@ checker, for each definition and theorem processed. If you ever find
 the system slowing down while processing a file, this can help you
 locate the source of the problem.
 
-** Making Auxiliary Facts Visible
-:PROPERTIES:
-  :CUSTOM_ID: Making_Auxiliary_Facts_Visible
-:END:
-
-We have seen that the =have= construct introduces an auxiliary subgoal
-in a proof, and is useful for structuring and documenting proofs.
-Given the term =have H : p, from s, t=, by default, the hypothesis =H=
-is not "visible" by automated procedures and tactics used to construct
-=t=. This is important because too much information may negatively
-affect the performance and effectiveness of automated procedures. You
-can make =H= available to automated procedures and tactics by using
-the idiom =assert H : p, from s, t=. Here is an example:
-#+BEGIN_SRC lean
-example (p q r : Prop) : p ∧ q ∧ r → q ∧ p :=
-assume Hpqr : p ∧ q ∧ r,
-assert Hp   : p,     from and.elim_left Hpqr,
-have   Hqr  : q ∧ r, from and.elim_right Hpqr,
-assert Hq   : q,     from and.elim_left Hqr,
-proof
-  -- Hp and Hq are visible here,
-  -- Hqr is not because we used "have".
-  and.intro Hq Hp
-qed
-#+END_SRC
-Recall that =proof ... qed= block is implemented using tactics,
-so any hypothesis introduced using =have= is invisible inside it.
-In the example above, =Hqr= is not visible in the =proof ... qed=
-block.
-
-The =have=, =show= and =assert= terms have a variant which provide
-even more control over which hypotheses are available in =from s=.
-#+BEGIN_SRC text
-have   H : p, using H_1 ... H_n, from s, t
-assert H : p, using H_1 ... H_n, from s, t
-show   H : p, using H_1 ... H_n, from s
-#+END_SRC
-In all three terms, the hypotheses =H_1= ... =H_n= are available for
-automated procedures and tactics used in =s=.
-#+BEGIN_SRC lean
-example (p q r : Prop) : p ∧ q ∧ r → q ∧ p :=
-assume Hpqr : p ∧ q ∧ r,
-have   Hp   : p,      from and.elim_left Hpqr,
-have   Hqr  : q ∧ r,  from and.elim_right Hpqr,
-assert Hq   : q,      from and.elim_left Hqr,
-show q ∧ p, using Hp, from
-proof
-  -- Hp is visible here because of =using Hp=
-  and.intro Hq Hp
-qed
-#+END_SRC
-See Chapter [[file:11_Tactics-Style_Proofs.org::#Tactic-Style_Proofs][Tactic-Style Proofs]] for a discussion of Lean's tactics.
-
-There are even situations where an auxiliary fact needs to be visible
-to the elaborator, so that it can solve unification problems that
-arise. This can arise when the expression to be synthesized depends on
-an auxiliary fact, =H=. We will see an example of this in Section
-[[file:11_Axioms.org::#Choice_Axioms][Choice Axioms]], when we discuss the Hilbert choice operator.
+# This section is no longer valid.
+#
+# ** Making Auxiliary Facts Visible
+# :PROPERTIES:
+#   :CUSTOM_ID: Making_Auxiliary_Facts_Visible
+# :END:
+
+# We have seen that the =have= construct introduces an auxiliary subgoal
+# in a proof, and is useful for structuring and documenting proofs.
+# Given the term =have H : p, from s, t=, by default, the hypothesis =H=
+# is not "visible" by automated procedures and tactics used to construct
+# =t=. This is important because too much information may negatively
+# affect the performance and effectiveness of automated procedures. You
+# can make =H= available to automated procedures and tactics by using
+# the idiom =assert H : p, from s, t=. Here is an example:
+# #+BEGIN_SRC lean
+# example (p q r : Prop) : p ∧ q ∧ r → q ∧ p :=
+# assume Hpqr : p ∧ q ∧ r,
+# assert Hp   : p,     from and.elim_left Hpqr,
+# have   Hqr  : q ∧ r, from and.elim_right Hpqr,
+# assert Hq   : q,     from and.elim_left Hqr,
+# proof
+#   -- Hp and Hq are visible here,
+#   -- Hqr is not because we used "have".
+#   and.intro Hq Hp
+# qed
+# #+END_SRC
+# Recall that =proof ... qed= block is implemented using tactics,
+# so any hypothesis introduced using =have= is invisible inside it.
+# In the example above, =Hqr= is not visible in the =proof ... qed=
+# block.
+
+# The =have=, =show= and =assert= terms have a variant which provide
+# even more control over which hypotheses are available in =from s=.
+# #+BEGIN_SRC text
+# have   H : p, using H_1 ... H_n, from s, t
+# assert H : p, using H_1 ... H_n, from s, t
+# show   H : p, using H_1 ... H_n, from s
+# #+END_SRC
+# In all three terms, the hypotheses =H_1= ... =H_n= are available for
+# automated procedures and tactics used in =s=.
+# #+BEGIN_SRC lean
+# example (p q r : Prop) : p ∧ q ∧ r → q ∧ p :=
+# assume Hpqr : p ∧ q ∧ r,
+# have   Hp   : p,      from and.elim_left Hpqr,
+# have   Hqr  : q ∧ r,  from and.elim_right Hpqr,
+# assert Hq   : q,      from and.elim_left Hqr,
+# show q ∧ p, using Hp, from
+# proof
+#   -- Hp is visible here because of =using Hp=
+#   and.intro Hq Hp
+# qed
+# #+END_SRC
+# See Chapter [[file:11_Tactics-Style_Proofs.org::#Tactic-Style_Proofs][Tactic-Style Proofs]] for a discussion of Lean's tactics.
+
+# There are even situations where an auxiliary fact needs to be visible
+# to the elaborator, so that it can solve unification problems that
+# arise. This can arise when the expression to be synthesized depends on
+# an auxiliary fact, =H=. We will see an example of this in Section
+# [[file:11_Axioms.org::#Choice_Axioms][Choice Axioms]] when we discuss the Hilbert choice operator.
 
 ** Sections
 
diff --git a/11_Tactic-Style_Proofs.org b/11_Tactic-Style_Proofs.org
index e0793e18..da7d4b2c 100644
--- a/11_Tactic-Style_Proofs.org
+++ b/11_Tactic-Style_Proofs.org
@@ -432,46 +432,48 @@ end
 # out proofs by induction, when it is often needed to obtain
 # the right induction hypothesis.
 
-** Managing Auxiliary Facts
-
-Recall from Section [[file:08_Building_Theories_and_Proofs.org::#Making_Auxiliary_Facts_Visible][Making Auxiliary Facts Visible]] that we need to use
-=assert= instead of =have= to state auxiliary subgoals if we wish to
-use them in tactic proofs. For example, the following proofs fail, if
-we replace any =assert= by a =have=:
-#+BEGIN_SRC lean
-example (p q : Prop) (H : p ∧ q) : p ∧ q ∧ p :=
-assert Hp : p, from and.left H,
-assert Hq : q, from and.right H,
-begin
-  apply (and.intro Hp),
-  apply (and.intro Hq),
-  exact Hp
-end
-
-example (p q : Prop) (H : p ∧ q) : p ∧ q ∧ p :=
-assert Hp : p, from and.left H,
-assert Hq : q, from and.right H,
-begin
-  apply and.intro,
-  assumption,
-  apply and.intro,
-  repeat assumption
-end
-#+END_SRC
-Alternatively, we can explicitly put a =have= statement into the
-context with the keyword =using=:
-#+BEGIN_SRC lean
-example (p q : Prop) (H : p ∧ q) : p ∧ q ∧ p :=
-have Hp : p, from and.left H,
-have Hq : q, from and.right H,
-show _, using Hp Hq,
-begin
-  apply and.intro,
-  assumption,
-  apply and.intro,
-  repeat assumption
-end
-#+END_SRC
+# This section is no longer valid!
+#
+# ** Managing Auxiliary Facts
+
+# Recall from Section [[file:08_Building_Theories_and_Proofs.org::#Making_Auxiliary_Facts_Visible][Making Auxiliary Facts Visible]] that we need to use
+# =assert= instead of =have= to state auxiliary subgoals if we wish to
+# use them in tactic proofs. For example, the following proofs fail, if
+# we replace any =assert= by a =have=:
+# #+BEGIN_SRC lean
+# example (p q : Prop) (H : p ∧ q) : p ∧ q ∧ p :=
+# assert Hp : p, from and.left H,
+# assert Hq : q, from and.right H,
+# begin
+#   apply (and.intro Hp),
+#   apply (and.intro Hq),
+#   exact Hp
+# end
+
+# example (p q : Prop) (H : p ∧ q) : p ∧ q ∧ p :=
+# assert Hp : p, from and.left H,
+# assert Hq : q, from and.right H,
+# begin
+#   apply and.intro,
+#   assumption,
+#   apply and.intro,
+#   repeat assumption
+# end
+# #+END_SRC
+# Alternatively, we can explicitly put a =have= statement into the
+# context with the keyword =using=:
+# #+BEGIN_SRC lean
+# example (p q : Prop) (H : p ∧ q) : p ∧ q ∧ p :=
+# have Hp : p, from and.left H,
+# have Hq : q, from and.right H,
+# show _, using Hp Hq,
+# begin
+#   apply and.intro,
+#   assumption,
+#   apply and.intro,
+#   repeat assumption
+# end
+# #+END_SRC
 
 ** Structuring Tactic Proofs
 
diff --git a/12_Axioms.org b/12_Axioms.org
index 4da5ad5c..3bc47690 100644
--- a/12_Axioms.org
+++ b/12_Axioms.org
@@ -789,58 +789,60 @@ epsilon_spec H
 end hide
 #+END_SRC
 
-In Section [[file:08_Building_Theories_and_Proofs.org::#Making_Auxiliary_Facts_Visible][Making Auxiliary Facts Visible]], we explained that, on some
-occasions, it is necessary to use =assert= instead of =have= to put
-auxiliary goals into the context so that the elaborator can find
-them. This often comes up in connection to =epsilon= and =some=,
-because these induce dependencies on elements of =Prop=. The following
-examples illustrate some of the places where =assert= is needed. A
-good rule of thumb is that if you are using =some= or =epsilon=, and
-you are presented with a strange error message, trying changing =have=
-to =assert=.
-
-#+BEGIN_SRC lean
-open classical
-
-section
-  variable A : Type
-  variable a : A
-
-  -- o.k.
-  example : ∃ x : A, x = x :=
-  have H1 : ∃ y, y = y, from exists.intro a rfl,
-  have H2 : some H1 = some H1, from some_spec H1,
-  exists.intro (some H1) H2
-
-  /-
-  -- invalid local context
-  example : ∃ x : A, x = x :=
-  have H1 : ∃ y, y = y, from exists.intro a rfl,
-  have H2 : some H1 = some H1, from some_spec H1,
-  exists.intro _ H2
-  -/
-
-  -- o.k.
-  example : ∃ x : A, x = x :=
-  assert H1 : ∃ y, y = y, from exists.intro a rfl,
-  have H2 : some H1 = some H1, from some_spec H1,
-  exists.intro _ H2
-
-  /-
-  -- invalid local context
-  example : ∃ x : A, x = x :=
-  have H1 : ∃ y, y = y, from exists.intro a rfl,
-  have H2 : some H1 = some H1, from some_spec H1,
-  exists.intro (some H1) (eq.trans H2 H2)
-  -/
-
-  -- o.k.
-  example : ∃ x : A, x = x :=
-  assert H1 : ∃ y, y = y, from exists.intro a rfl,
-  have H2 : some H1 = some H1, from some_spec H1,
-  exists.intro (some H1) (eq.trans H2 H2)
-end
-#+END_SRC
+# This is no longer the case.
+#
+# In Section [[file:08_Building_Theories_and_Proofs.org::#Making_Auxiliary_Facts_Visible][Making Auxiliary Facts Visible]], we explained that, on some
+# occasions, it is necessary to use =assert= instead of =have= to put
+# auxiliary goals into the context so that the elaborator can find
+# them. This often comes up in connection to =epsilon= and =some=,
+# because these induce dependencies on elements of =Prop=. The following
+# examples illustrate some of the places where =assert= is needed. A
+# good rule of thumb is that if you are using =some= or =epsilon=, and
+# you are presented with a strange error message, trying changing =have=
+# to =assert=.
+
+# #+BEGIN_SRC lean
+# open classical
+
+# section
+#   variable A : Type
+#   variable a : A
+
+#   -- o.k.
+#   example : ∃ x : A, x = x :=
+#   have H1 : ∃ y, y = y, from exists.intro a rfl,
+#   have H2 : some H1 = some H1, from some_spec H1,
+#   exists.intro (some H1) H2
+
+#   /-
+#   -- invalid local context
+#   example : ∃ x : A, x = x :=
+#   have H1 : ∃ y, y = y, from exists.intro a rfl,
+#   have H2 : some H1 = some H1, from some_spec H1,
+#   exists.intro _ H2
+#   -/
+
+#   -- o.k.
+#   example : ∃ x : A, x = x :=
+#   assert H1 : ∃ y, y = y, from exists.intro a rfl,
+#   have H2 : some H1 = some H1, from some_spec H1,
+#   exists.intro _ H2
+
+#   /-
+#   -- invalid local context
+#   example : ∃ x : A, x = x :=
+#   have H1 : ∃ y, y = y, from exists.intro a rfl,
+#   have H2 : some H1 = some H1, from some_spec H1,
+#   exists.intro (some H1) (eq.trans H2 H2)
+#   -/
+
+#   -- o.k.
+#   example : ∃ x : A, x = x :=
+#   assert H1 : ∃ y, y = y, from exists.intro a rfl,
+#   have H2 : some H1 = some H1, from some_spec H1,
+#   exists.intro (some H1) (eq.trans H2 H2)
+# end
+# #+END_SRC
 
 ** Excluded Middle
 
diff --git a/13_More_Tactics.org b/13_More_Tactics.org
index a1b85124..cce2ddf5 100644
--- a/13_More_Tactics.org
+++ b/13_More_Tactics.org
@@ -253,32 +253,34 @@ the introduction rule for =true=, respectively.
 
 Combinators are used to combine tactics. The most basic one is the
 =and_then= combinator, written with a semicolon (=;=), which applies tactics
-successively. This is not the same as listing tactics separated by
-commas in a =begin ... end= block, since when multiple solutions are
-available, =and_then= will backtrack until it finds a solution or
-exhausts all the possibilities. The following example fails if we
-replace the semicolon by a comma:
-#+BEGIN_SRC lean
-example (p q : Prop) (Hq : q) : p ∨ q :=
-begin constructor; assumption end
-#+END_SRC
-The =constructor= tactic creates a /stream/ of outcomes, one for each
-possible result. A comma forces the tactic to commit to an answer at
-that point, whereas the semicolon causes Lean to systematically try
-all the possibilities. Here is a more elaborate example:
-#+BEGIN_SRC lean
-variable p : nat → Prop
-variable q : nat → Prop
-variables a b c : nat
-
-example : p c → p b → q b → p a → ∃ x, p x ∧ q x :=
-by intros; apply exists.intro; split; eassumption; eassumption
-#+END_SRC
-The =eassumption= tactic is stronger than =assumption= in that it is
-more aggressive when it comes to reducing expressions, and in that it
-returns a stream of solutions rather than the first one that
-matches. In this case, the first solution that matches =p ?x= is
-ultimately not the right choice, and backtracking is crucial.
+successively. 
+
+# This is not the same as listing tactics separated by
+# commas in a =begin ... end= block, since when multiple solutions are
+# available, =and_then= will backtrack until it finds a solution or
+# exhausts all the possibilities. The following example fails if we
+# replace the semicolon by a comma:
+# #+BEGIN_SRC lean
+# example (p q : Prop) (Hq : q) : p ∨ q :=
+# begin constructor; assumption end
+# #+END_SRC
+# The =constructor= tactic creates a /stream/ of outcomes, one for each
+# possible result. A comma forces the tactic to commit to an answer at
+# that point, whereas the semicolon causes Lean to systematically try
+# all the possibilities. Here is a more elaborate example:
+# #+BEGIN_SRC lean
+# variable p : nat → Prop
+# variable q : nat → Prop
+# variables a b c : nat
+
+# example : p c → p b → q b → p a → ∃ x, p x ∧ q x :=
+# by intros; apply exists.intro; split; eassumption; eassumption
+# #+END_SRC
+# The =eassumption= tactic is stronger than =assumption= in that it is
+# more aggressive when it comes to reducing expressions, and in that it
+# returns a stream of solutions rather than the first one that
+# matches. In this case, the first solution that matches =p ?x= is
+# ultimately not the right choice, and backtracking is crucial.
 
 The =par= combinator, written with a vertical bar (=|=), tries one tactic and then the other,
 using the first one that succeeds. The =repeat= tactic applies a
@@ -297,7 +299,7 @@ open set function eq.ops
 
 variables {X Y Z : Type}
 
-lemma image_compose (f : Y → X) (g : X → Y) (a : set X) : (f ∘ g) ' a = f ' (g ' a) :=
+lemma image_comp (f : Y → X) (g : X → Y) (a : set X) : (f ∘ g) ' a = f ' (g ' a) :=
 set.ext (take z,
   iff.intro
     (assume Hz,
@@ -305,7 +307,7 @@ set.ext (take z,
       by repeat (apply mem_image | assumption | reflexivity))
     (assume Hz,
       obtain y [x Hz₁ Hz₂] Hy₂, from Hz,
-      by repeat (apply mem_image | assumption | esimp [compose] | rewrite Hz₂)))
+      by repeat (apply mem_image | assumption | esimp [comp] | rewrite Hz₂)))
 #+END_SRC
 
 # TODO: need more and better examples, both above and below.