doc-src/TutorialI/document/documents.tex
changeset 48522 708278fc2dff
parent 48521 0e4bb86c74fd
child 48523 ec3e2ff58a85
--- a/doc-src/TutorialI/document/documents.tex	Thu Jul 26 17:32:28 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-
-\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: