| author | Thomas Lindae <thomas.lindae@in.tum.de> |
| Wed, 17 Jul 2024 21:02:30 +0200 | |
| changeset 81077 | 664c1a6cc8c1 |
| parent 48985 | 5386df44a037 |
| permissions | -rw-r--r-- |
| 11647 | 1 |
|
| 12671 | 2 |
\chapter{Presenting Theories}
|
| 12570 | 3 |
\label{ch:thy-present}
|
4 |
||
| 12743 | 5 |
By now the reader should have become sufficiently acquainted with elementary |
| 12764 | 6 |
theory development in Isabelle/HOL\@. The following interlude describes |
7 |
how to present theories in a typographically |
|
| 12743 | 8 |
pleasing manner. Isabelle provides a rich infrastructure for concrete syntax |
9 |
of the underlying $\lambda$-calculus language (see |
|
| 12764 | 10 |
{\S}\ref{sec:concrete-syntax}), as well as document preparation of theory texts
|
| 12743 | 11 |
based on existing PDF-{\LaTeX} technology (see
|
| 12764 | 12 |
{\S}\ref{sec:document-preparation}).
|
| 12635 | 13 |
|
| 12743 | 14 |
As pointed out by Leibniz\index{Leibniz, Gottfried Wilhelm} more than 300
|
15 |
years ago, \emph{notions} are in principle more important than
|
|
16 |
\emph{notations}, but suggestive textual representation of ideas is vital to
|
|
17 |
reduce the mental effort to comprehend and apply them. |
|
| 11647 | 18 |
|
|
48966
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
48536
diff
changeset
|
19 |
\input{Documents.tex}
|
| 11647 | 20 |
|
21 |
%%% Local Variables: |
|
22 |
%%% mode: latex |
|
23 |
%%% TeX-master: t |
|
24 |
%%% End: |