# HG changeset patch
# User lcp
# Date 781950017 -3600
# Node ID c97f5a7cf76369c18fcd628d98199c926ef80805
# Parent  bb3f87f9cafea77390d4fe494ae41ab2b130ed7c
Moving theory LList to ex directory

diff -r bb3f87f9cafe -r c97f5a7cf763 doc-src/Logics/Old_HOL.tex
--- a/doc-src/Logics/Old_HOL.tex	Mon Oct 10 18:09:58 1994 +0100
+++ b/doc-src/Logics/Old_HOL.tex	Wed Oct 12 09:20:17 1994 +0100
@@ -1223,21 +1223,6 @@
 variable~$xs$ in subgoal~$i$.
 
 
-\subsection{The type constructor for lazy lists, {\tt llist}}
-\index{*llist type}
-
-The definition of lazy lists demonstrates methods for handling infinite
-data structures and coinduction in higher-order logic.  Theory
-\thydx{LList} defines an operator for corecursion on lazy lists, which is
-used to define a few simple functions such as map and append.  Corecursion
-cannot easily define operations such as filter, which can compute
-indefinitely before yielding the next element (if any!) of the lazy list.
-A coinduction principle is defined for proving equations on lazy lists.
-
-I have written a paper discussing the treatment of lazy lists; it also
-covers finite lists~\cite{paulson-coind}.
-
-
 \section{Datatype declarations}
 \index{*datatype|(}
 
@@ -1745,7 +1730,7 @@
 \end{ttbox}
 The HOL distribution contains many other inductive definitions, such as the
 theory {\tt HOL/ex/PropLog.thy} and the directory {\tt HOL/IMP}.  The
-theory {\tt HOL/LList.thy} contains coinductive definitions.
+theory {\tt HOL/ex/LList.thy} contains coinductive definitions.
 
 \index{*coinductive|)} \index{*inductive|)} \underscoreoff
 
@@ -1784,6 +1769,15 @@
 \item Theories {\tt InSort} and {\tt Qsort} prove correctness properties of
   insertion sort and quick sort.
 
+\item The definition of lazy lists demonstrates methods for handling
+  infinite data structures and coinduction in higher-order
+  logic~\cite{paulson-coind}.  Theory \thydx{LList} defines an operator for
+  corecursion on lazy lists, which is used to define a few simple functions
+  such as map and append.  Corecursion cannot easily define operations such
+  as filter, which can compute indefinitely before yielding the next
+  element (if any!) of the lazy list.  A coinduction principle is defined
+  for proving equations on lazy lists.
+
 \item Theory {\tt PropLog} proves the soundness and completeness of
   classical propositional logic, given a truth table semantics.  The only
   connective is $\imp$.  A Hilbert-style axiom system is specified, and its