1.1 --- a/doc-src/Logics/Old_HOL.tex	Thu Apr 17 18:10:12 1997 +0200
     1.2 +++ b/doc-src/Logics/Old_HOL.tex	Thu Apr 17 18:10:49 1997 +0200
     1.3 @@ -1567,7 +1567,7 @@
     1.4  An {\bf inductive definition} specifies the least set closed under given
     1.5  rules.  For example, a structural operational semantics is an inductive
     1.6  definition of an evaluation relation.  Dually, a {\bf coinductive
     1.7 -  definition} specifies the greatest set closed under given rules.  An
     1.8 +  definition} specifies the greatest set consistent with given rules.  An
     1.9  important example is using bisimulation relations to formalize equivalence
    1.10  of processes and infinite data structures.
    1.11