1.1 --- a/doc-src/extra.sty	Mon Jul 11 13:15:05 1994 +0200
     1.2 +++ b/doc-src/extra.sty	Mon Jul 11 16:29:21 1994 +0200
     1.3 @@ -13,7 +13,8 @@
     1.4  %\leftmargini is LaTeX's first-level indentation for items (2.5em)
     1.5  %@endparenv is LaTeX's trick for preventing indentation of next paragraph
     1.6  \newenvironment{ttbox}{\par\nobreak\vskip-2pt
     1.7 -           \vbox\bgroup\footnotesize\begin{alltt} \leftskip\leftmargini}%
     1.8 +           \vbox\bgroup\footnotesize\begin{alltt}\chardef\{=`\{\chardef\}=`\}%
     1.9 +             \leftskip\leftmargini}%
    1.10          {\end{alltt}\egroup\vskip-7pt\@endparenv}
    1.11  \newcommand\ttbreak{\end{ttbox}\vskip-10pt\begin{ttbox}}
    1.12  

     2.1 --- a/doc-src/ind-defs.tex	Mon Jul 11 13:15:05 1994 +0200
     2.2 +++ b/doc-src/ind-defs.tex	Mon Jul 11 16:29:21 1994 +0200
     2.3 @@ -1,5 +1,4 @@
     2.4  \documentstyle[a4,proof,iman,extra,times]{llncs}
     2.5 -%Repetition in the two sentences that begin ``The powerset operator''
     2.6  \newif\ifCADE
     2.7  \CADEtrue
     2.8  
     2.9 @@ -272,7 +271,7 @@
    2.10  
    2.11  \subsection{The fixedpoint definitions}
    2.12  The package translates the list of desired introduction rules into a fixedpoint
    2.13 -definition.  Consider, as a running example, the finite set operator
    2.14 +definition.  Consider, as a running example, the finite powerset operator
    2.15  $\Fin(A)$: the set of all finite subsets of~$A$.  It can be
    2.16  defined as the least set closed under the rules
    2.17  \[  \emptyset\in\Fin(A)  \qquad 
    2.18 @@ -494,12 +493,12 @@
    2.19  
    2.20  
    2.21  \section{Examples of inductive and coinductive definitions}\label{ind-eg-sec}
    2.22 -This section presents several examples: the finite set operator,
    2.23 +This section presents several examples: the finite powerset operator,
    2.24  lists of $n$ elements, bisimulations on lazy lists, the well-founded part
    2.25  of a relation, and the primitive recursive functions.
    2.26  
    2.27 -\subsection{The finite set operator}
    2.28 -The definition of finite sets has been discussed extensively above.  Here
    2.29 +\subsection{The finite powerset operator}
    2.30 +This operator has been discussed extensively above.  Here
    2.31  is the corresponding ML invocation (note that $\cons(a,b)$ abbreviates
    2.32  $\{a\}\un b$ in Isabelle/ZF):
    2.33  \begin{ttbox}

     3.1 --- a/doc-src/mathsing.sty	Mon Jul 11 13:15:05 1994 +0200
     3.2 +++ b/doc-src/mathsing.sty	Mon Jul 11 16:29:21 1994 +0200
     3.3 @@ -539,8 +539,10 @@
     3.4  \def\endlisting{\endtrivlist\baselineskip=\oldbaselineskip}
     3.5  
     3.6  %Add ttbox to Springer's macros!!  - LCP
     3.7 +%now redefines \{ and \}
     3.8  \newenvironment{ttbox}{\par\nobreak\vskip-2pt%
     3.9 -           \vbox\bgroup\begin{listing}\leftskip\leftmargini}%
    3.10 +           \vbox\bgroup\begin{listing}\chardef\{=`\{\chardef\}=`\}%
    3.11 +                      \leftskip\leftmargini}%
    3.12          {\end{listing}\egroup\vskip-7pt\@endparenv}
    3.13  \newcommand\ttbreak{\end{ttbox}\goodbreak\vskip-8pt plus 3pt\begin{ttbox}}
    3.14