# HG changeset patch
# User lcp
# Date 781950017 3600
# Node ID c97f5a7cf76369c18fcd628d98199c926ef80805
# Parent bb3f87f9cafea77390d4fe494ae41ab2b130ed7c
Moving theory LList to ex directory
diff r bb3f87f9cafe r c97f5a7cf763 docsrc/Logics/Old_HOL.tex
 a/docsrc/Logics/Old_HOL.tex Mon Oct 10 18:09:58 1994 +0100
+++ b/docsrc/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 higherorder 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{paulsoncoind}.


\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 higherorder
+ logic~\cite{paulsoncoind}. 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 Hilbertstyle axiom system is specified, and its