author | Walther Neuper <neuper@ist.tugraz.at> |
Thu, 12 Aug 2010 15:03:34 +0200 | |
branch | isac-from-Isabelle2009-2 |
changeset 37913 | 20e3616b2d9c |
parent 12764 | b43333dc6e7d |
child 49551 | 4e2ee88276d2 |
permissions | -rw-r--r-- |
wenzelm@11647 | 1 |
|
wenzelm@12671 | 2 |
\chapter{Presenting Theories} |
wenzelm@12570 | 3 |
\label{ch:thy-present} |
wenzelm@12570 | 4 |
|
wenzelm@12743 | 5 |
By now the reader should have become sufficiently acquainted with elementary |
paulson@12764 | 6 |
theory development in Isabelle/HOL\@. The following interlude describes |
paulson@12764 | 7 |
how to present theories in a typographically |
wenzelm@12743 | 8 |
pleasing manner. Isabelle provides a rich infrastructure for concrete syntax |
wenzelm@12743 | 9 |
of the underlying $\lambda$-calculus language (see |
paulson@12764 | 10 |
{\S}\ref{sec:concrete-syntax}), as well as document preparation of theory texts |
wenzelm@12743 | 11 |
based on existing PDF-{\LaTeX} technology (see |
paulson@12764 | 12 |
{\S}\ref{sec:document-preparation}). |
wenzelm@12635 | 13 |
|
wenzelm@12743 | 14 |
As pointed out by Leibniz\index{Leibniz, Gottfried Wilhelm} more than 300 |
wenzelm@12743 | 15 |
years ago, \emph{notions} are in principle more important than |
wenzelm@12743 | 16 |
\emph{notations}, but suggestive textual representation of ideas is vital to |
wenzelm@12743 | 17 |
reduce the mental effort to comprehend and apply them. |
wenzelm@11647 | 18 |
|
wenzelm@11647 | 19 |
\input{Documents/document/Documents.tex} |
wenzelm@11647 | 20 |
|
wenzelm@11647 | 21 |
%%% Local Variables: |
wenzelm@11647 | 22 |
%%% mode: latex |
wenzelm@11647 | 23 |
%%% TeX-master: t |
wenzelm@11647 | 24 |
%%% End: |