diff -r 5f810292c030 -r ccae8c659762 doc-src/Inductive/ind-defs.tex
--- a/doc-src/Inductive/ind-defs.tex	Mon May 10 17:45:16 1999 +0200
+++ b/doc-src/Inductive/ind-defs.tex	Tue May 11 10:32:10 1999 +0200
@@ -582,7 +582,7 @@
   domains   "listn(A)" <= "nat*list(A)"
   intrs
     NilI  "<0,Nil>: listn(A)"
-    ConsI "[| a: A;  <n,l>: listn(A) |] ==> <succ(n), Cons(a,l)>: listn(A)"
+    ConsI "[| a:A; <n,l>:listn(A) |] ==> <succ(n), Cons(a,l)>: listn(A)"
   type_intrs "nat_typechecks @ list.intrs"
 end
 \end{ttbox}
@@ -696,15 +696,17 @@
 \]
 To make this coinductive definition, the theory file includes (after the
 declaration of $\llist(A)$) the following lines:
+\bgroup\leftmargini=\parindent
 \begin{ttbox}
 consts    lleq :: i=>i
 coinductive
   domains "lleq(A)" <= "llist(A) * llist(A)"
   intrs
     LNil  "<LNil,LNil> : lleq(A)"
-    LCons "[| a:A; <l,l'>: lleq(A) |] ==> <LCons(a,l),LCons(a,l')>: lleq(A)"
+    LCons "[| a:A; <l,l'>:lleq(A) |] ==> <LCons(a,l),LCons(a,l')>: lleq(A)"
   type_intrs  "llist.intrs"
 \end{ttbox}
+\egroup
 The domain of $\lleq(A)$ is $\llist(A)\times\llist(A)$.  The type-checking
 rules include the introduction rules for $\llist(A)$, whose 
 declaration is discussed below (\S\ref{lists-sec}).
@@ -830,27 +832,29 @@
 
 \begin{figure}
 \begin{ttbox}
-Primrec = List +
-consts
-  primrec :: i
-  SC      :: i
-  \(\vdots\)
+Primrec_defs = Main +
+consts SC :: i
+ \(\vdots\)
 defs
-  SC_def    "SC == lam l:list(nat).list_case(0, \%x xs.succ(x), l)"
-  \(\vdots\)
+ SC_def    "SC == lam l:list(nat).list_case(0, \%x xs.succ(x), l)"
+ \(\vdots\)
+end
+
+Primrec = Primrec_defs +
+consts prim_rec :: i
 inductive
-  domains "primrec" <= "list(nat)->nat"
-  intrs
-    SC       "SC : primrec"
-    CONST    "k: nat ==> CONST(k) : primrec"
-    PROJ     "i: nat ==> PROJ(i) : primrec"
-    COMP     "[| g: primrec; fs: list(primrec) |] ==> COMP(g,fs): primrec"
-    PREC     "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec"
-  monos       list_mono
-  con_defs    SC_def, CONST_def, PROJ_def, COMP_def, PREC_def
-  type_intrs "nat_typechecks @ list.intrs @                      
-              [lam_type, list_case_type, drop_type, map_type,    
-               apply_type, rec_type]"
+ domains "primrec" <= "list(nat)->nat"
+ intrs
+   SC     "SC : primrec"
+   CONST  "k: nat ==> CONST(k) : primrec"
+   PROJ   "i: nat ==> PROJ(i) : primrec"
+   COMP   "[| g: primrec; fs: list(primrec) |] ==> COMP(g,fs): primrec"
+   PREC   "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec"
+ monos       list_mono
+ con_defs    SC_def, CONST_def, PROJ_def, COMP_def, PREC_def
+ type_intrs "nat_typechecks @ list.intrs @                      
+             [lam_type, list_case_type, drop_type, map_type,    
+              apply_type, rec_type]"
 end
 \end{ttbox}
 \hrule
@@ -937,7 +941,7 @@
 $\QInl(a)$ and $\QInr(b)$ for $a$, $b\in\quniv(A)$.  In a typical codatatype
 definition with set parameters $A_1$, \ldots, $A_k$, a suitable domain is
 $\quniv(A_1\un\cdots\un A_k)$.  Details are published
-elsewhere~\cite{paulson-final}.
+elsewhere~\cite{paulson-mscs}.
 
 \subsection{The case analysis operator}
 The (co)datatype package automatically defines a case analysis operator,
@@ -1000,7 +1004,7 @@
 \ifshort
 Now $\lst(A)$ is a datatype and enjoys the usual induction rule.
 \else
-Since $\lst(A)$ is a datatype, it enjoys a structural induction rule, {\tt
+Since $\lst(A)$ is a datatype, it has a structural induction rule, {\tt
   list.induct}:
 \[ \infer{P(x)}{x\in\lst(A) & P(\Nil)
         & \infer*{P(\Cons(a,l))}{[a\in A & l\in\lst(A) & P(l)]_{a,l}} }
@@ -1079,7 +1083,7 @@
          \right]_{t,f}} }
 \] 
 This rule establishes a single predicate for $\TF(A)$, the union of the
-recursive sets.  Although such reasoning is sometimes useful
+recursive sets.  Although such reasoning can be useful
 \cite[\S4.5]{paulson-set-II}, a proper mutual induction rule should establish
 separate predicates for $\tree(A)$ and $\forest(A)$.  The package calls this
 rule {\tt tree\_forest.mutual\_induct}.  Observe the usage of $P$ and $Q$ in
@@ -1292,7 +1296,7 @@
 Isabelle/\textsc{zf} instead uses a variant notion of ordered pairing, which
 can be generalized to a variant notion of function.  Elsewhere I have
 proved that this simple approach works (yielding final coalgebras) for a broad
-class of definitions~\cite{paulson-final}.
+class of definitions~\cite{paulson-mscs}.
 
 Several large studies make heavy use of inductive definitions.  L\"otzbeyer
 and Sandner have formalized two chapters of a semantics book~\cite{winskel93},
@@ -1318,15 +1322,12 @@
 The approach is not restricted to set theory.  It should be suitable for any
 logic that has some notion of set and the Knaster-Tarski theorem.  I have
 ported the (co)inductive definition package from Isabelle/\textsc{zf} to
-Isabelle/\textsc{hol} (higher-order logic).  V\"olker~\cite{voelker95}
-is investigating how to port the (co)datatype package.  \textsc{hol}
-represents sets by unary predicates; defining the corresponding types may
-cause complications.
+Isabelle/\textsc{hol} (higher-order logic).  
 
 
 \begin{footnotesize}
 \bibliographystyle{springer}
-\bibliography{string-abbrv,atp,theory,funprog,isabelle,crossref}
+\bibliography{../manual}
 \end{footnotesize}
 %%%%%\doendnotes