|
11647
|
1 |
|
|
12570
|
2 |
\chapter{Presenting theories}
|
|
|
3 |
\label{ch:thy-present}
|
|
|
4 |
|
|
12653
|
5 |
By virtue of the previous chapters the reader has become sufficiently
|
|
|
6 |
acquainted with basic formal theory development in Isabelle/HOL. The
|
|
|
7 |
subsequent interlude covers the ``marginal'' issue of presenting theories in a
|
|
|
8 |
typographically pleasing manner. Isabelle provides a rich infrastructure for
|
|
|
9 |
concrete syntax (input and output of the $\lambda$-calculus language), as well
|
|
|
10 |
as document preparation of theory texts based on existing PDF-{\LaTeX}
|
|
|
11 |
technology.
|
|
12635
|
12 |
|
|
|
13 |
As has been pointed out by Leibniz\index{Leibniz, Gottfried Wilhelm} more than
|
|
|
14 |
300 years ago, \emph{notions} are in principle more important than
|
|
|
15 |
\emph{notations}, but fair textual representation of ideas is very important
|
|
|
16 |
to reduce the mental effort in actual applications.
|
|
11647
|
17 |
|
|
|
18 |
\input{Documents/document/Documents.tex}
|
|
|
19 |
|
|
|
20 |
%%% Local Variables:
|
|
|
21 |
%%% mode: latex
|
|
|
22 |
%%% TeX-master: t
|
|
|
23 |
%%% End:
|