# HG changeset patch
# User paulson
# Date 848681045 -3600
# Node ID 5687d7dec139bb8409f8c8f3a648f4d5e26b9a9a
# Parent  36bb751913c6bf808ec3f32e30e97388b0353081
Minor textual improvements; updating of a reference

diff -r 36bb751913c6 -r 5687d7dec139 doc-src/ind-defs.tex
--- a/doc-src/ind-defs.tex	Fri Nov 22 17:41:32 1996 +0100
+++ b/doc-src/ind-defs.tex	Fri Nov 22 17:44:05 1996 +0100
@@ -136,7 +136,7 @@
 Such data structures are called \defn{datatypes}
 below, by analogy with datatype declarations in Standard~\textsc{ml}\@.
 Some logics take datatypes as primitive; consider Boyer and Moore's shell
-principle~\cite{bm79} and the Coq type theory~\cite{paulin92}.
+principle~\cite{bm79} and the Coq type theory~\cite{paulin-tlca}.
 
 A datatype is but one example of an \defn{inductive definition}.  This
 specifies the least set closed under given rules~\cite{aczel77}.  The
@@ -144,7 +144,7 @@
 operational semantics~\cite{hennessy90} is an inductive definition of a
 reduction or evaluation relation on programs.  A few theorem provers
 provide commands for formalizing inductive definitions; these include
-Coq~\cite{paulin92} and again the \textsc{hol} system~\cite{camilleri92}.
+Coq~\cite{paulin-tlca} and again the \textsc{hol} system~\cite{camilleri92}.
 
 The dual notion is that of a \defn{coinductive definition}.  This specifies
 the greatest set closed under given rules.  Important examples include
@@ -246,7 +246,7 @@
 \ldots,~$p_k$.  Each recursive set then has the form $R_i(\vec{p})$.  The
 parameters must be identical every time they occur within a definition.  This
 would appear to be a serious restriction compared with other systems such as
-Coq~\cite{paulin92}.  For instance, we cannot define the lists of
+Coq~\cite{paulin-tlca}.  For instance, we cannot define the lists of
 $n$ elements as the set $\listn(A,n)$ using rules where the parameter~$n$
 varies.  Section~\ref{listn-sec} describes how to express this set using the
 inductive definition package.
@@ -549,7 +549,7 @@
 
 \subsection{Lists of $n$ elements}\label{listn-sec}
 This has become a standard example of an inductive definition.  Following
-Paulin-Mohring~\cite{paulin92}, we could attempt to define a new datatype
+Paulin-Mohring~\cite{paulin-tlca}, we could attempt to define a new datatype
 $\listn(A,n)$, for lists of length~$n$, as an $n$-indexed family of sets.
 But her introduction rules
 \[ \hbox{\tt Niln}\in\listn(A,0)  \qquad
@@ -735,7 +735,7 @@
 all $\prec$-predecessors of~$a$, for $a\in D$.  Thus we need an
 introduction rule of the form 
 \[ \infer{a\in\acc(\prec)}{\forall y.y\prec a\imp y\in\acc(\prec)} \]
-Paulin-Mohring treats this example in Coq~\cite{paulin92}, but it causes
+Paulin-Mohring treats this example in Coq~\cite{paulin-tlca}, but it causes
 difficulties for other systems.  Its premise is not acceptable to the
 inductive definition package of the Cambridge \textsc{hol}
 system~\cite{camilleri92}.  It is also unacceptable to the Isabelle package
@@ -1212,7 +1212,7 @@
 \textsc{alf} requires new rules for each definition~\cite{dybjer91}.  With Coq
 the situation is subtler still; its underlying Calculus of Constructions can
 express inductive definitions~\cite{huet88}, but cannot quite handle datatype
-definitions~\cite{paulin92}.  It seems that researchers tried hard to
+definitions~\cite{paulin-tlca}.  It seems that researchers tried hard to
 circumvent these problems before finally extending the Calculus with rule
 schemes for strictly positive operators.  Recently Gim{\'e}nez has extended
 the Calculus of Constructions with inductive and coinductive
@@ -1414,7 +1414,7 @@
   type_intrs {\it introduction rules for type-checking}
   type_elims {\it elimination rules for type-checking}
 \end{ttbox}
-A coinductive definition is identical save that it starts with the keyword
+A coinductive definition is identical, but starts with the keyword
 {\tt coinductive}.  
 
 The {\tt monos}, {\tt con\_defs}, {\tt type\_intrs} and {\tt type\_elims}
@@ -1549,8 +1549,8 @@
   $\quniv(A_1\un\cdots\un A_k)$ is used for a codatatype definition.
 
   These choices should work for all finitely-branching (co)datatype
-  definitions.  For examples of infinitely-branching datatype
-  definitions, see the file {\tt ZF/ex/Brouwer.thy}.
+  definitions.  For examples of infinitely-branching datatypes, 
+  see file {\tt ZF/ex/Brouwer.thy}.
 
 \item[\it datatype declaration] has the form
 \begin{quote}