diff --git a/src/Naturals.lagda b/src/Naturals.lagda
index 85bd51df..321343e7 100644
--- a/src/Naturals.lagda
+++ b/src/Naturals.lagda
@@ -204,7 +204,7 @@ A philosopher might note that our reference to the first day, second
 day, and so on, implicitly involves an understanding of natural
 numbers.  In this sense, our definition might indeed be regarded as in
 some sense circular.  We won't worry about the philosophy, but are ok
-with taking some intuitive notions--such as counting--as given.
+with taking some intuitive notions---such as counting---as given.
 
 While the natural numbers have been understood for as long as people
 could count, the inductive definition of the natural numbers is relatively
@@ -217,7 +217,7 @@ presented by a new method), published the following year.
 
 ## A useful pragma
 
-In Agda, any line beginning `--`, or any code enclosed between `{-`
+In Agda, any text following `--` or enclosed between `{-`
 and `-}` is considered a *comment*.  Comments have no effect on the
 code, with the exception of one special kind of comment, called a
 *pragma*, which is enclosed between `{-#` and `#-}`.
diff --git a/src/Properties.lagda b/src/Properties.lagda
index 72ac262f..6163c19b 100644
--- a/src/Properties.lagda
+++ b/src/Properties.lagda
@@ -78,7 +78,7 @@ data ℕ : Set where
   zero : ℕ
   suc : ℕ → ℕ
 \end{code}
-This tells us that `zero` is a natural--the *base case*--and that if
+This tells us that `zero` is a natural---the *base case*---and that if
 `m` is a natural then `suc m` is also a natural---the *inductive
 case*.