1 2\chapter{Presenting Theories} 3\label{ch:thy-present} 4 5By now the reader should have become sufficiently acquainted with elementary 6theory development in Isabelle/HOL\@. The following interlude describes 7how to present theories in a typographically 8pleasing manner. Isabelle provides a rich infrastructure for concrete syntax 9of the underlying $\lambda$-calculus language (see 10{\S}\ref{sec:concrete-syntax}), as well as document preparation of theory texts 11based on existing PDF-{\LaTeX} technology (see 12{\S}\ref{sec:document-preparation}). 13 14As pointed out by Leibniz\index{Leibniz, Gottfried Wilhelm} more than 300 15years ago, \emph{notions} are in principle more important than 16\emph{notations}, but suggestive textual representation of ideas is vital to 17reduce the mental effort to comprehend and apply them. 18 19\input{Documents.tex} 20 21%%% Local Variables: 22%%% mode: latex 23%%% TeX-master: t 24%%% End: 25