author paulson Thu, 17 Apr 1997 18:10:49 +0200 changeset 2975 230f456956a2 parent 2974 bb55cab416af child 2976 7c848e330a80
Corrected the informal description of coinductive definition
 doc-src/Logics/HOL.tex file | annotate | diff | comparison | revisions doc-src/Logics/Old_HOL.tex file | annotate | diff | comparison | revisions
--- 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
--- 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.