diff -r 0c86acc069ad -r 5deda0549f97 doc-src/TutorialI/document/documents.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/document/documents.tex	Thu Jul 26 17:16:02 2012 +0200
@@ -0,0 +1,24 @@
+
+\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: