# HG changeset patch
# User paulson
# Date 846670674 -3600
# Node ID afc15c2fd5b5865746c384c97042e563edff11c8
# Parent  217ae06dc291bbacfbde039e2c4b4a3867c158ca
Minor updates

diff -r 217ae06dc291 -r afc15c2fd5b5 doc-src/ind-defs.tex
--- a/doc-src/ind-defs.tex	Wed Oct 30 11:15:09 1996 +0100
+++ b/doc-src/ind-defs.tex	Wed Oct 30 11:17:54 1996 +0100
@@ -1,5 +1,5 @@
 \documentstyle[a4,alltt,iman,extra,proof209,12pt]{article}
-\newif\ifshort
+\newif\ifshort%''Short'' means a published version, not the documentation
 \shortfalse%%%%%\shorttrue
 
 \title{A Fixedpoint Approach to\\ 
@@ -170,7 +170,8 @@
 thus accepting all provably monotone inductive definitions, including
 iterated definitions.
 
-The package has been implemented in Isabelle~\cite{isabelle-intro} using
+The package has been implemented in
+Isabelle~\cite{paulson-markt,paulson-isa-book} using 
 \textsc{zf} set theory \cite{paulson-set-I,paulson-set-II}; part of it has
 since been ported to Isabelle/\textsc{hol} (higher-order logic).  The
 recursion equations are specified as introduction rules for the mutually
@@ -1299,9 +1300,10 @@
 definitions (of arithmetic expressions, boolean expressions and commands) and
 three inductive definitions (the corresponding operational rules).  Using
 different techniques, Nipkow~\cite{nipkow-CR} and Rasmussen~\cite{rasmussen95}
-have both proved the Church-Rosser theorem.  A datatype specifies the set of
-$\lambda$-terms, while inductive definitions specify several reduction
-relations.
+have both proved the Church-Rosser theorem; inductive definitions specify
+several reduction relations on $\lambda$-terms.  Recently, I have applied
+inductive definitions to the analysis of cryptographic
+protocols~\cite{paulson-markt}. 
 
 To demonstrate coinductive definitions, Frost~\cite{frost95} has proved the
 consistency of the dynamic and static semantics for a small functional