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