src/Doc/Tutorial/document/documents0.tex

combinator List.those;
simprule for case distinction on Option.map expression

\chapter{Presenting Theories}
\label{ch:thy-present}

By now the reader should have become sufficiently acquainted with elementary
theory development in Isabelle/HOL\@.  The following interlude describes
how to present theories in a typographically
pleasing manner.  Isabelle provides a rich infrastructure for concrete syntax
of the underlying $\lambda$-calculus language (see
{\S}\ref{sec:concrete-syntax}), as well as document preparation of theory texts
based on existing PDF-{\LaTeX} technology (see
{\S}\ref{sec:document-preparation}).

As pointed out by Leibniz\index{Leibniz, Gottfried Wilhelm} more than 300
years ago, \emph{notions} are in principle more important than
\emph{notations}, but suggestive textual representation of ideas is vital to
reduce the mental effort to comprehend and apply them.

\input{Documents.tex}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: