1.1 --- a/doc-src/Logics/Old_HOL.tex	Mon Oct 10 18:09:58 1994 +0100
     1.2 +++ b/doc-src/Logics/Old_HOL.tex	Wed Oct 12 09:20:17 1994 +0100
     1.3 @@ -1223,21 +1223,6 @@
     1.4  variable~$xs$ in subgoal~$i$.
     1.5  
     1.6  
     1.7 -\subsection{The type constructor for lazy lists, {\tt llist}}
     1.8 -\index{*llist type}
     1.9 -
    1.10 -The definition of lazy lists demonstrates methods for handling infinite
    1.11 -data structures and coinduction in higher-order logic.  Theory
    1.12 -\thydx{LList} defines an operator for corecursion on lazy lists, which is
    1.13 -used to define a few simple functions such as map and append.  Corecursion
    1.14 -cannot easily define operations such as filter, which can compute
    1.15 -indefinitely before yielding the next element (if any!) of the lazy list.
    1.16 -A coinduction principle is defined for proving equations on lazy lists.
    1.17 -
    1.18 -I have written a paper discussing the treatment of lazy lists; it also
    1.19 -covers finite lists~\cite{paulson-coind}.
    1.20 -
    1.21 -
    1.22  \section{Datatype declarations}
    1.23  \index{*datatype|(}
    1.24  
    1.25 @@ -1745,7 +1730,7 @@
    1.26  \end{ttbox}
    1.27  The HOL distribution contains many other inductive definitions, such as the
    1.28  theory {\tt HOL/ex/PropLog.thy} and the directory {\tt HOL/IMP}.  The
    1.29 -theory {\tt HOL/LList.thy} contains coinductive definitions.
    1.30 +theory {\tt HOL/ex/LList.thy} contains coinductive definitions.
    1.31  
    1.32  \index{*coinductive|)} \index{*inductive|)} \underscoreoff
    1.33  
    1.34 @@ -1784,6 +1769,15 @@
    1.35  \item Theories {\tt InSort} and {\tt Qsort} prove correctness properties of
    1.36    insertion sort and quick sort.
    1.37  
    1.38 +\item The definition of lazy lists demonstrates methods for handling
    1.39 +  infinite data structures and coinduction in higher-order
    1.40 +  logic~\cite{paulson-coind}.  Theory \thydx{LList} defines an operator for
    1.41 +  corecursion on lazy lists, which is used to define a few simple functions
    1.42 +  such as map and append.  Corecursion cannot easily define operations such
    1.43 +  as filter, which can compute indefinitely before yielding the next
    1.44 +  element (if any!) of the lazy list.  A coinduction principle is defined
    1.45 +  for proving equations on lazy lists.
    1.46 +
    1.47  \item Theory {\tt PropLog} proves the soundness and completeness of
    1.48    classical propositional logic, given a truth table semantics.  The only
    1.49    connective is $\imp$.  A Hilbert-style axiom system is specified, and its