doc-src/Logics/HOL.tex

 substructure of the main theory structure.
 
 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.
 
 

 
 \item[\tt mk_cases] is a function to create simplified instances of {\tt
 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.
 
 \begin{figure}

      pred "pred a r: Pow(acc r) ==> a: acc r"
   monos   "[Pow_mono]"
 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|)}
 
 
 \section{The examples directories}

 Directory {\tt HOL/IMP} contains a formalization of various denotational,
 operational and axiomatic semantics of a simple while-language, the necessary
 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.
 
 Directory {\tt HOL/MiniML} contains a formalization of the type system of the