Minor updates
Wed, 30 Oct 1996 11:17:54 +0100
changeset 2137 afc15c2fd5b5
parent 2136 217ae06dc291
child 2138 056dead45ae8
Minor updates
--- 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 @@
+\newif\ifshort%''Short'' means a published version, not the documentation
 \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
+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
 To demonstrate coinductive definitions, Frost~\cite{frost95} has proved the
 consistency of the dynamic and static semantics for a small functional