diff --git a/doc/tl/tl.bib b/doc/tl/tl.bib
index 931ffbb1d..bf0bee99b 100644
--- a/doc/tl/tl.bib
+++ b/doc/tl/tl.bib
@@ -18,11 +18,11 @@
 @InProceedings{	  beer.01.cav,
   author	= {Ilan Beer and Shoham Ben-David and Cindy Eisner and Dana
 		  Fisman and Anna Gringauze and Yoav Rodeh},
-  title		= {The Temporal Logic Sugar},
+  title		= {The Temporal Logic {S}ugar},
   booktitle	= {Proceedings of the 13th international conferance on
 		  Computer Aided Verification (CAV'01)},
   series	= {Lecture Notes in Computer Science},
-  editor	= {Berry, Gérard and Comon, Hubert and Finkel, Alain},
+  editor	= {Berry, G{\'e}rard and Comon, Hubert and Finkel, Alain},
   publisher	= {Springer},
   isbn		= {978-3-540-42345-4},
   pages		= {363--367},
diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex
index f625d82bd..44be3006b 100644
--- a/doc/tl/tl.tex
+++ b/doc/tl/tl.tex
@@ -193,7 +193,7 @@
 
 \section{Finite and Infinite Sequences}
 
-Let $\N=\{0,1,2,\ldots\}$ designate the set of natural numbers and
+Let $\N=\{0,1,2,\ldots\}$ denote the set of natural numbers and
 $\omega\not\in\N$ the first transfinite ordinal.  We extend the $<$
 relation from $\N$ to $\N\cup\{\omega\}$ with $\forall n\in N,\,
 n<\omega$.  Similarly let us extend the addition and subtraction with
@@ -1005,8 +1005,8 @@ suffix-closed, i.e., if you remove any finite prefix of an accepted
 $\varphi$ is a suffix-closed formula, then $\G\varphi \equiv \varphi$.
 
 
-Let $\varphi$ designate any arbitrary formula and $\varphi_E$
-(resp. $\varphi_U$) designate any instance of a pure eventuality
+Let $\varphi$ denote any arbitrary formula and $\varphi_E$
+(resp. $\varphi_U$) denote any instance of a pure eventuality
 (resp. a purely universal) formula.  We have the following grammar
 rules:
 
@@ -1108,9 +1108,9 @@ methods \texttt{is\_syntactic\_safety()},
 page~\pageref{property-methods}).
 
 The symbols $\varphi_G$, $\varphi_S$, $\varphi_O$, $\varphi_P$,
-$\varphi_R$ designate any formula belonging respectively to the
+$\varphi_R$ denot any formula belonging respectively to the
 Guarantee, Safety, Obligation, Persistence, or Recurrence classes.
-$\varphi_F$ designates a finite LTL formula (the unnamed class at the
+$\varphi_F$ denotes a finite LTL formula (the unnamed class at the
 intersection of Safety and Guarantee formul\ae{} on
 Fig.~\ref{fig:hierarchy}).  $v$ denotes any variable, $r$ any SERE,
 $r_F$ any bounded SERE (no loops), and $r_I$ any unbounded SERE.
@@ -1164,7 +1164,7 @@ $r_F$ any bounded SERE (no loops), and $r_I$ any unbounded SERE.
            \mid{}& \X\varphi_R \mid \G\varphi_R \mid
                    \varphi_R\U\varphi_G\mid\varphi_R\R\varphi_R\mid
                    \varphi_R\W\varphi_R\mid\varphi_G\M\varphi_R\\
-           \mid{}& \sere{r_F}\Esuffix \varphi_R \mid \sere{r_I}\Esuffix \varphi_G\mid \sere{r}\Asuffix \varphi_P\\
+           \mid{}& \sere{r}\Asuffix \varphi_R\mid \sere{r_F}\Esuffix \varphi_R \mid \sere{r_I}\Esuffix \varphi_G\\
 \end{align*}
 
 It should be noted that a formula can belong to a class of the
@@ -1293,16 +1293,16 @@ from left to right, as usual):
   \G(f_1\OR\ldots\OR f_n \OR \G\F(g_1)\OR\ldots\OR \G\F(g_m)) & \equiv \G(f_1\OR\ldots\OR f_n)\OR \G\F(g_1\OR\ldots\OR g_m)
 \end{align*}
 
-Note that the latter three rewriting rules for $\G$ have no dual:
-rewriting $\F(f \AND \G\F g)$ to $\F(f) \AND \G\F(g)$ (as suggested
-by~\citet{somenzi.00.cav}) goes against our goal of moving the $\F$
-operator in front of the formula.  Conceptually, it is also easier to
-understand $\F(f \AND \G\F g)$: has long as $f$ has not been verified,
-there is no need to worry about the $\G\F g$ term.
+% Note that the latter three rewriting rules for $\G$ have no dual:
+% rewriting $\F(f \AND \G\F g)$ to $\F(f) \AND \G\F(g)$ (as suggested
+% by~\citet{somenzi.00.cav}) goes against our goal of moving the $\F$
+% operator in front of the formula.  Conceptually, it is also easier to
+% understand $\F(f \AND \G\F g)$: has long as $f$ has not been verified,
+% there is no need to worry about the $\G\F g$ term.
 
 Here are the basic rewriting rules for binary operators (excluding
 $\OR$ and $\AND$ which are considered in Spot as $n$-ary operators).
-$b$ denotes a Boolean formula.
+$b$ denotes any Boolean formula.
 
 \begin{align*}
   \1 \U f             & \equiv \F f            & f \W \0             & \equiv \G f            \\
@@ -1684,8 +1684,8 @@ f)\implies(\pi\VDash g)$.
 
 The recursive rules for syntactic implication are rules are described
 in table~\ref{tab:syntimpl}, in which $\simp$ denotes the syntactic
-implication, $f$, $f_1$, $f_2$, $g$, $g_1$ and $g_2$ designate any PSL
-formula in negative normal form, and $f_U$ and $g_E$ designate a
+implication, $f$, $f_1$, $f_2$, $g$, $g_1$ and $g_2$ denote any PSL
+formula in negative normal form, and $f_U$ and $g_E$ denot a
 purely universal formula and a pure eventuality.
 
 The form on the left of the table syntactically implies the form on
@@ -1704,7 +1704,7 @@ conclusion by chaining two rules: ``$\F f \simp \underbrace{\F
 ``$f \simp \F g$ \textit{if} $f\simp g$''.
 
 The rules from table~\ref{tab:syntimpl} should be completed by the
-following cases, where $f_b$ and $g_b$ designate Boolean formul\ae{}:
+following cases, where $f_b$ and $g_b$ denote Boolean formul\ae{}:
 \begin{center}
 \begin{tabular}{rl}
 we have                       & if                                    \\