diff --git a/doc/01.tex b/doc/01.tex
index ceacbb5aa..43c83be24 100644
--- a/doc/01.tex
+++ b/doc/01.tex
@@ -74,10 +74,8 @@ Abstract syntax:
 
 $$
 \begin{array}{rcll}
-  \mathscr X & = & \{x, y, z, \dots\}            & \mbox{(variables)}\\
-  \otimes    & = & \{\lstinline|+|, \lstinline|-|, \lstinline|*|, \lstinline|/|, \lstinline|%|,
-                     \lstinline|<|, \lstinline|<=|, \lstinline|>|, \lstinline|>=|, \lstinline|==|,
-                     \lstinline|!=|, \lstinline|!!|, \lstinline|&&|\} & \mbox{(binary operators)}\\
+  \mathscr X & = & \{x,\, y,\, z,\, \dots\}            & \mbox{(variables)}\\
+  \otimes    & = & \{+,\, -,\, \times,\, /,\, \%,\, <,\, \le,\, >,\, \ge,\, =,\,\ne,\, \vee,\, \wedge\} & \mbox{(binary operators)}\\
    \mathscr E & = & \mathscr X                    & \mbox{(expressions)}\\
               &   & \mathbb N                     & \\
               &   & \mathscr E \otimes \mathscr E & 
@@ -108,19 +106,19 @@ $$
 \begin{tabular}{c|cl}
   $\otimes$     & $\oplus$ in ocaml\\
   \hline
-  \lstinline|+|  & \lstinline|+|   \\
-  \lstinline|-|  & \lstinline|-|   \\
-  \lstinline|*|  & \lstinline|*|   \\
-  \lstinline|/|  & \lstinline|/|   \\
-  \lstinline|%|  & \lstinline|mod| \\
-  \lstinline|<|  & \lstinline|<|  & \rdelim\}{6}{5mm}[  see note 1 below] \\
-  \lstinline|>|  & \lstinline|>|   \\
-  \lstinline|<=| & \lstinline|<=|  \\
-  \lstinline|>=| & \lstinline|>=|  \\
-  \lstinline|==| & \lstinline|=|   \\
-  \lstinline|!=| & \lstinline|<>|  \\
-  \lstinline|&&| & \lstinline|&&| & \rdelim\}{2}{5mm}[  see note 2 below]\\
-  \lstinline|!!| & \lstinline/||/ 
+  $+$      & \lstinline|+|   \\
+  $-$      & \lstinline|-|   \\
+  $\times$ & \lstinline|*|   \\
+  $/$      & \lstinline|/|   \\
+  $\%$     & \lstinline|mod| \\
+  $<$      & \lstinline|<|  & \rdelim\}{6}{5mm}[  see note 1 below] \\
+  $>$      & \lstinline|>|   \\
+  $\le$    & \lstinline|<=|  \\
+  $\ge$    & \lstinline|>=|  \\
+  $=$      & \lstinline|=|   \\
+  $\ne$    & \lstinline|<>|  \\
+  $\wedge$ & \lstinline|&&| & \rdelim\}{2}{5mm}[  see note 2 below]\\
+  $\vee$   & \lstinline/||/ 
 \end{tabular}
 \end{center}
 
@@ -140,5 +138,5 @@ Important observations:
   \item $\otimes$ is an element of language \emph{syntax}, while $\oplus$ is its interpretation in the meta-language of
   semanic description (simpler: in the language of interpreter implementation).
   \item This concrete semantics is \emph{strict}: for a binary operator both its arguments are evaluated unconditionally; thus,
-  for example, \lstinline|1 !! x| is undefined in empty state.
+  for example, \lstinline|1$\,\vee\,$x| is undefined in empty state.
 \end{enumerate}
diff --git a/doc/02.tex b/doc/02.tex
index 43f117af6..67140fa41 100644
--- a/doc/02.tex
+++ b/doc/02.tex
@@ -48,14 +48,14 @@ With the relation ``$\Rightarrow$'' defined we can abbreviate the ``surface'' se
 \setarrow{\xRightarrow}
 
 \[
-\forall S\in\mathscr S,\,\forall i\in\mathbb Z^*\;:\;\sembr{S}_{\mathscr S} i = o \Leftrightarrow \trans{\inbr{\bot, i, \epsilon}}{S}{\inbr{\_, \_, o}}
+\forall S\in\mathscr S,\,\forall \iota\in\mathbb Z^*\;:\;\sembr{S}_{\mathscr S} \iota = o \Leftrightarrow \trans{\inbr{\bot, i, \epsilon}}{S}{\inbr{\_, \_, o}}
 \]
 
 
 \begin{figure}[t]
-\[\trans{\inbr{s, i, o}}{\llang{x := $\;\;e$}}{\inbr{s[x\gets\sembr{e}_{\mathscr E}\;s], i, o}}\ruleno{Assign}\]
-\[\trans{\inbr{s, z\llang{::}i, o}}{\llang{read ($x$)}}{\inbr{s[x\gets z], i, o}}\ruleno{Read}\]
-\[\trans{\inbr{s, i, o}}{\llang{write ($e$)}}{\inbr{s, i, o \llang{@} \sembr{e}_{\mathscr E}\;s}}\ruleno{Write}\]
+\[\trans{\inbr{\sigma,\, \iota,\, o}}{\llang{x := $\;\;e$}}{\inbr{\sigma\,[x\gets\sembr{e}_{\mathscr E}\;\sigma],\, \iota,\, o}}\ruleno{Assign}\]
+\[\trans{\inbr{\sigma,\, z\iota,\, o}}{\llang{read ($x$)}}{\inbr{\sigma\,[x\gets z],\, \iota,\, o}}\ruleno{Read}\]
+\[\trans{\inbr{\sigma,\, \iota,\, o}}{\llang{write ($e$)}}{\inbr{\sigma,\, \iota,\, o(\sembr{e}_{\mathscr E}\;\sigma)}}\ruleno{Write}\]
 \[\trule{\trans{c_1}{S_1}{c^\prime},\;\trans{c^\prime}{S_2}{c_2}}{\trans{c_1}{S_1\llang{;}S_2}{c_2}}\ruleno{Seq}\]
 \caption{Big-step operational semantics for statements}
 \label{bs_stmt}
diff --git a/doc/lectures.tex b/doc/lectures.tex
index 6865ef6a4..e4f7f8b16 100644
--- a/doc/lectures.tex
+++ b/doc/lectures.tex
@@ -77,7 +77,7 @@
 
 \lstdefinelanguage{ocaml}{
 keywords={let, begin, end, in, match, type, and, fun, 
-function, try, with, class, object, method, of, rec, repeat, until,
+function, try, mod, with, class, object, method, of, rec, repeat, until,
 while, not, do, done, as, val, inherit, module, sig, @type, struct, 
 if, then, else, open, virtual, new, fresh, skip, od, fi, elif, for, local, return, read, write, fi, case, esac, od},
 sensitive=true,