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:
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
