diff --git a/doc/spec/01.introduction.tex b/doc/spec/01.introduction.tex
index b8fa8b314..0685f508a 100644
--- a/doc/spec/01.introduction.tex
+++ b/doc/spec/01.introduction.tex
@@ -1,5 +1,23 @@
 \chapter{Introduction}
 
-\input{01.01.general_characteristics}
-\input{01.02.notation}
-\input{01.03.values}
+\lama is a programming language developed by JetBrains Research for education purposes. Its general characteristics are:
+
+\begin{itemize}
+\item procedural with first-class functions~--- functions can be passed as arguments, placed in data structures,
+  returned and constructed at runtime via closures mechanism;
+\item with lexical static scoping;
+\item strict~--- all arguments of function application are evaluated before function body;
+\item imperative~--- variables can be re-assigned, function calls can have side effects;
+\item untyped~--- no static type checking is performed;
+\item with S-expressions and pattern-matching;
+\item with user-defined infix operators, including those defined in local scopes;
+\item with automatic memory management (garbage collection).
+\end{itemize}
+
+The name \lama is an acronym for $\lambda\textsc{-Algol}$ since the language has borrowed the syntactic shape of
+operators from \textsc{Algol-68}; \textsc{Haskell}~\cite{haskell} and \textsc{OCaml}~\cite{ocaml} can be
+mentioned as other languages of inspiration.
+
+%\input{01.01.general_characteristics}
+%\input{01.02.notation}
+%\input{01.03.values}
diff --git a/doc/spec/04.extensions.tex b/doc/spec/04.extensions.tex
index 9b80e6b9b..07976b911 100644
--- a/doc/spec/04.extensions.tex
+++ b/doc/spec/04.extensions.tex
@@ -94,6 +94,39 @@ where "$x$"~--- a fresh variable which does not occur free in "$e$".
 
 \section{Dot Notation}
 
-\section{Mutable Closures}
+A function call
+
+\begin{lstlisting}
+    $f$ ($e_1$, ..., $e_k$)
+\end{lstlisting}
+
+where $f$~--- an identifier~--- can be rewritten as
+
+\begin{lstlisting}
+    $e_1$.$f$ ($e_2$, ..., $e_k$)
+\end{lstlisting}
+
+In particular, a call to a one-argument function $f (e)$ can be rewritten as $e.f$.
 
 \section{Patterns in Function Arguments}
+
+Patterns can be used in function argument specification: a declaration
+
+\begin{lstlisting}
+    fun f ($p_1$, ..., $p_k$) { e }
+\end{lstlisting}
+
+is equivalent to
+
+\begin{lstlisting}
+    fun f ($x_1$, ..., $x_k$) {
+      case $x_1$ of
+        $p_1$ -> case $x_2$ of
+                   ... -> e
+                 esac
+      esac
+    }
+\end{lstlisting}
+
+where $x_i$~--- fresh variables, not free in $e$.
+
diff --git a/doc/spec/spec.tex b/doc/spec/spec.tex
index ded3dfac2..7de807ccb 100644
--- a/doc/spec/spec.tex
+++ b/doc/spec/spec.tex
@@ -195,7 +195,7 @@ language=alm
 \tableofcontents
 
 \input{01.introduction}
-\input{02.abstract_syntax_and_semantics}
+%\input{02.abstract_syntax_and_semantics}
 \input{03.concrete_syntax}
 \input{04.extensions}
 \input{05.driver_options}