doc-src/TutorialI/Documents/documents.tex

added configuration options;

+
−
+
−\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/document/Documents.tex}
+
−
+
−%%% Local Variables: 
+
−%%% mode: latex
+
−%%% TeX-master: t
+
−%%% End: