doc-src/Logics/Old_HOL.tex
 changeset 629 c97f5a7cf763 parent 600 d9133e7ed38a child 705 9fb068497df4
--- 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