--- 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.