1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/TutorialI/Documents/documents.tex	Thu Jul 26 18:55:42 2012 +0200
     1.3 @@ -0,0 +1,24 @@
     1.4 +
     1.5 +\chapter{Presenting Theories}
     1.6 +\label{ch:thy-present}
     1.7 +
     1.8 +By now the reader should have become sufficiently acquainted with elementary
     1.9 +theory development in Isabelle/HOL\@.  The following interlude describes
    1.10 +how to present theories in a typographically
    1.11 +pleasing manner.  Isabelle provides a rich infrastructure for concrete syntax
    1.12 +of the underlying $\lambda$-calculus language (see
    1.13 +{\S}\ref{sec:concrete-syntax}), as well as document preparation of theory texts
    1.14 +based on existing PDF-{\LaTeX} technology (see
    1.15 +{\S}\ref{sec:document-preparation}).
    1.16 +
    1.17 +As pointed out by Leibniz\index{Leibniz, Gottfried Wilhelm} more than 300
    1.18 +years ago, \emph{notions} are in principle more important than
    1.19 +\emph{notations}, but suggestive textual representation of ideas is vital to
    1.20 +reduce the mental effort to comprehend and apply them.
    1.21 +
    1.22 +\input{document/Documents.tex}
    1.23 +
    1.24 +%%% Local Variables: 
    1.25 +%%% mode: latex
    1.26 +%%% TeX-master: t
    1.27 +%%% End: