# HG changeset patch
# User lcp
# Date 773936961 -7200
# Node ID 466dd59b3645fa45b666ac9fd3911b29a7fcc574
# Parent  0d19ab250cc9a904357cbe976acfd91180bab782
misc updates

diff -r 0d19ab250cc9 -r 466dd59b3645 doc-src/extra.sty
--- a/doc-src/extra.sty	Mon Jul 11 13:15:05 1994 +0200
+++ b/doc-src/extra.sty	Mon Jul 11 16:29:21 1994 +0200
@@ -13,7 +13,8 @@
 %\leftmargini is LaTeX's first-level indentation for items (2.5em)
 %@endparenv is LaTeX's trick for preventing indentation of next paragraph
 \newenvironment{ttbox}{\par\nobreak\vskip-2pt
-           \vbox\bgroup\footnotesize\begin{alltt} \leftskip\leftmargini}%
+           \vbox\bgroup\footnotesize\begin{alltt}\chardef\{=`\{\chardef\}=`\}%
+             \leftskip\leftmargini}%
         {\end{alltt}\egroup\vskip-7pt\@endparenv}
 \newcommand\ttbreak{\end{ttbox}\vskip-10pt\begin{ttbox}}
 
diff -r 0d19ab250cc9 -r 466dd59b3645 doc-src/ind-defs.tex
--- a/doc-src/ind-defs.tex	Mon Jul 11 13:15:05 1994 +0200
+++ b/doc-src/ind-defs.tex	Mon Jul 11 16:29:21 1994 +0200
@@ -1,5 +1,4 @@
 \documentstyle[a4,proof,iman,extra,times]{llncs}
-%Repetition in the two sentences that begin ``The powerset operator''
 \newif\ifCADE
 \CADEtrue
 
@@ -272,7 +271,7 @@
 
 \subsection{The fixedpoint definitions}
 The package translates the list of desired introduction rules into a fixedpoint
-definition.  Consider, as a running example, the finite set operator
+definition.  Consider, as a running example, the finite powerset operator
 $\Fin(A)$: the set of all finite subsets of~$A$.  It can be
 defined as the least set closed under the rules
 \[  \emptyset\in\Fin(A)  \qquad 
@@ -494,12 +493,12 @@
 
 
 \section{Examples of inductive and coinductive definitions}\label{ind-eg-sec}
-This section presents several examples: the finite set operator,
+This section presents several examples: the finite powerset operator,
 lists of $n$ elements, bisimulations on lazy lists, the well-founded part
 of a relation, and the primitive recursive functions.
 
-\subsection{The finite set operator}
-The definition of finite sets has been discussed extensively above.  Here
+\subsection{The finite powerset operator}
+This operator has been discussed extensively above.  Here
 is the corresponding ML invocation (note that $\cons(a,b)$ abbreviates
 $\{a\}\un b$ in Isabelle/ZF):
 \begin{ttbox}
diff -r 0d19ab250cc9 -r 466dd59b3645 doc-src/mathsing.sty
--- a/doc-src/mathsing.sty	Mon Jul 11 13:15:05 1994 +0200
+++ b/doc-src/mathsing.sty	Mon Jul 11 16:29:21 1994 +0200
@@ -539,8 +539,10 @@
 \def\endlisting{\endtrivlist\baselineskip=\oldbaselineskip}
 
 %Add ttbox to Springer's macros!!  - LCP
+%now redefines \{ and \}
 \newenvironment{ttbox}{\par\nobreak\vskip-2pt%
-           \vbox\bgroup\begin{listing}\leftskip\leftmargini}%
+           \vbox\bgroup\begin{listing}\chardef\{=`\{\chardef\}=`\}%
+                      \leftskip\leftmargini}%
         {\end{listing}\egroup\vskip-7pt\@endparenv}
 \newcommand\ttbreak{\end{ttbox}\goodbreak\vskip-8pt plus 3pt\begin{ttbox}}