1.1 --- a/doc-src/ind-defs.tex	Mon Jul 11 13:15:05 1994 +0200
     1.2 +++ b/doc-src/ind-defs.tex	Mon Jul 11 16:29:21 1994 +0200
     1.3 @@ -1,5 +1,4 @@
     1.4  \documentstyle[a4,proof,iman,extra,times]{llncs}
     1.5 -%Repetition in the two sentences that begin ``The powerset operator''
     1.6  \newif\ifCADE
     1.7  \CADEtrue
     1.8  
     1.9 @@ -272,7 +271,7 @@
    1.10  
    1.11  \subsection{The fixedpoint definitions}
    1.12  The package translates the list of desired introduction rules into a fixedpoint
    1.13 -definition.  Consider, as a running example, the finite set operator
    1.14 +definition.  Consider, as a running example, the finite powerset operator
    1.15  $\Fin(A)$: the set of all finite subsets of~$A$.  It can be
    1.16  defined as the least set closed under the rules
    1.17  \[  \emptyset\in\Fin(A)  \qquad 
    1.18 @@ -494,12 +493,12 @@
    1.19  
    1.20  
    1.21  \section{Examples of inductive and coinductive definitions}\label{ind-eg-sec}
    1.22 -This section presents several examples: the finite set operator,
    1.23 +This section presents several examples: the finite powerset operator,
    1.24  lists of $n$ elements, bisimulations on lazy lists, the well-founded part
    1.25  of a relation, and the primitive recursive functions.
    1.26  
    1.27 -\subsection{The finite set operator}
    1.28 -The definition of finite sets has been discussed extensively above.  Here
    1.29 +\subsection{The finite powerset operator}
    1.30 +This operator has been discussed extensively above.  Here
    1.31  is the corresponding ML invocation (note that $\cons(a,b)$ abbreviates
    1.32  $\{a\}\un b$ in Isabelle/ZF):
    1.33  \begin{ttbox}