--- a/doc-src/Logics/HOL.tex Thu Apr 10 14:26:01 1997 +0200
+++ b/doc-src/Logics/HOL.tex Thu Apr 10 18:07:27 1997 +0200
@@ -1864,7 +1864,7 @@
This package is derived from the ZF one, described in a
separate paper,\footnote{It appeared in CADE~\cite{paulson-CADE} and a
longer version is distributed with Isabelle.} which you should refer to
-in case of difficulties. The package is simpler than ZF's, thanks to HOL's
+in case of difficulties. The package is simpler than ZF's thanks to HOL's
automatic type-checking. The type of the (co)inductive determines the
domain of the fixedpoint definition, and the package does not use inference
rules for type-checking.
@@ -1893,9 +1893,10 @@
elim}, using freeness reasoning on some underlying datatype.
\end{description}
-For an inductive definition, the result structure contains two induction rules,
-{\tt induct} and \verb|mutual_induct|. For a coinductive definition, it
-contains the rule \verb|coinduct|.
+For an inductive definition, the result structure contains two induction
+rules, {\tt induct} and \verb|mutual_induct|. (To save storage, the latter
+rule is just {\tt True} unless more than one set is being defined.) For a
+coinductive definition, it contains the rule \verb|coinduct|.
Figure~\ref{def-result-fig} summarizes the two result signatures,
specifying the types of all these components.
@@ -2003,8 +2004,9 @@
end
\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/ex/LList.thy} contains coinductive definitions.
+theory {\tt HOL/ex/PropLog.thy} and the subdirectories {\tt IMP}, {\tt Lambda}
+and {\tt Auth}. The theory {\tt HOL/ex/LList.thy} contains coinductive
+definitions.
\index{*coinductive|)} \index{*inductive|)}
@@ -2023,7 +2025,7 @@
equivalence proofs, soundness and completeness of the Hoare rules w.r.t.\ the
denotational semantics, and soundness and completeness of a verification
condition generator. Much of development is taken from
-Winskel~\cite{winskel93}. For details see~\cite{Nipkow-FSTTCS-96}.
+Winskel~\cite{winskel93}. For details see~\cite{nipkow-IMP}.
Directory {\tt HOL/Hoare} contains a user friendly surface syntax for Hoare
logic, including a tactic for generating verification-conditions.
--- a/doc-src/Logics/logics.bbl Thu Apr 10 14:26:01 1997 +0200
+++ b/doc-src/Logics/logics.bbl Thu Apr 10 18:07:27 1997 +0200
@@ -126,11 +126,37 @@
\newblock {\em Intuitionistic type theory}.
\newblock Bibliopolis, 1984.
+\bibitem{milner78}
+Robin Milner.
+\newblock A theory of type polymorphism in programming.
+\newblock {\em Journal of Computer and System Sciences}, 17:348--375, 1978.
+
\bibitem{milner-coind}
Robin Milner and Mads Tofte.
\newblock Co-induction in relational semantics.
\newblock {\em Theoretical Computer Science}, 87:209--220, 1991.
+\bibitem{nazareth-nipkow}
+Dieter Nazareth and Tobias Nipkow.
+\newblock Formal verification of algorithm {W}: The monomorphic case.
+\newblock In J.~von Wright, J.~Grundy, and J.~Harrison, editors, {\em Theorem
+ Proving in Higher Order Logics: {TPHOLs} '96}, LNCS 1125, pages 331--345,
+ 1996.
+
+\bibitem{Nipkow-CR}
+Tobias Nipkow.
+\newblock More {Church-Rosser} proofs (in {Isabelle/HOL}).
+\newblock In Michael McRobbie and John~K. Slaney, editors, {\em Automated
+ Deduction --- {CADE}-13 International Conference}, LNAI 1104, pages 733--747.
+ Springer, 1996.
+
+\bibitem{nipkow-IMP}
+Tobias Nipkow.
+\newblock Winskel is (almost) right: Towards a mechanized semantics textbook.
+\newblock In V.~Chandru and V.~Vinay, editors, {\em Foundations of Software
+ Technology and Theoretical Computer Science}, volume 1180 of {\em LNCS},
+ pages 180--192. Springer, 1996.
+
\bibitem{noel}
Philippe No{\"e}l.
\newblock Experimenting with {Isabelle} in {ZF} set theory.
@@ -173,10 +199,23 @@
\newblock Set theory for verification: {II}. {Induction} and recursion.
\newblock {\em Journal of Automated Reasoning}, 15(2):167--215, 1995.
+\bibitem{paulson-ns}
+Lawrence~C. Paulson.
+\newblock Mechanized proofs of security protocols: {Needham-Schroeder} with
+ public keys.
+\newblock Technical Report 413, Computer Laboratory, University of Cambridge,
+ January 1997.
+
\bibitem{paulson-coind}
Lawrence~C. Paulson.
\newblock Mechanizing coinduction and corecursion in higher-order logic.
-\newblock {\em Journal of Logic and Computation}, 7(2), March 1997.
+\newblock {\em Journal of Logic and Computation}, 7(2):175--204, March 1997.
+
+\bibitem{paulson-security}
+Lawrence~C. Paulson.
+\newblock Proving properties of security protocols by induction.
+\newblock In {\em 10th Computer Security Foundations Workshop}. IEEE Computer
+ Society Press, 1997.
\newblock In press.
\bibitem{paulson-COLOG}
@@ -197,7 +236,7 @@
F.~J. Pelletier.
\newblock Seventy-five problems for testing automatic theorem provers.
\newblock {\em Journal of Automated Reasoning}, 2:191--216, 1986.
-\newblock Errata, JAR 4 (1988), 235--236.
+\newblock Errata, JAR 4 (1988), 235--236 and JAR 18 (1997), 135.
\bibitem{plaisted90}
David~A. Plaisted.
--- a/doc-src/Logics/logics.tex Thu Apr 10 14:26:01 1997 +0200
+++ b/doc-src/Logics/logics.tex Thu Apr 10 18:07:27 1997 +0200
@@ -61,6 +61,6 @@
%%\include{Cube}
%%\include{LCF}
\bibliographystyle{plain}
-\bibliography{string,atp,theory,funprog,logicprog,isabelle,crossref}
+\bibliography{string,general,atp,theory,funprog,logicprog,isabelle,crossref}
\input{logics.ind}
\end{document}