# HG changeset patch
# User paulson
# Date 861293449 -7200
# Node ID 230f456956a27232025d66de91fe683ad4e13213
# Parent  bb55cab416af79b7de5a9f0854684037f627365f
Corrected the informal description of coinductive definition

diff -r bb55cab416af -r 230f456956a2 doc-src/Logics/HOL.tex
--- a/doc-src/Logics/HOL.tex	Thu Apr 17 18:10:12 1997 +0200
+++ b/doc-src/Logics/HOL.tex	Thu Apr 17 18:10:49 1997 +0200
@@ -1845,12 +1845,14 @@
 \index{*inductive|(}
 \index{*coinductive|(}
 
-An {\bf inductive definition} specifies the least set closed under given
-rules.  For example, a structural operational semantics is an inductive
-definition of an evaluation relation.  Dually, a {\bf coinductive
-  definition} specifies the greatest set closed under given rules.  An
-important example is using bisimulation relations to formalize equivalence
-of processes and infinite data structures.
+An {\bf inductive definition} specifies the least set~$R$ closed under given
+rules.  (Applying a rule to elements of~$R$ yields a result within~$R$.)  For
+example, a structural operational semantics is an inductive definition of an
+evaluation relation.  Dually, a {\bf coinductive definition} specifies the
+greatest set~$R$ consistent with given rules.  (Every element of~$R$ can be
+seen as arising by applying a rule to elements of~$R$.)  An important example
+is using bisimulation relations to formalize equivalence of processes and
+infinite data structures.
 
 A theory file may contain any number of inductive and coinductive
 definitions.  They may be intermixed with other declarations; in
diff -r bb55cab416af -r 230f456956a2 doc-src/Logics/Old_HOL.tex
--- a/doc-src/Logics/Old_HOL.tex	Thu Apr 17 18:10:12 1997 +0200
+++ b/doc-src/Logics/Old_HOL.tex	Thu Apr 17 18:10:49 1997 +0200
@@ -1567,7 +1567,7 @@
 An {\bf inductive definition} specifies the least set closed under given
 rules.  For example, a structural operational semantics is an inductive
 definition of an evaluation relation.  Dually, a {\bf coinductive
-  definition} specifies the greatest set closed under given rules.  An
+  definition} specifies the greatest set consistent with given rules.  An
 important example is using bisimulation relations to formalize equivalence
 of processes and infinite data structures.