--- a/ProgTutorial/Essential.thy Wed Dec 02 17:08:37 2009 +0100
+++ b/ProgTutorial/Essential.thy Thu Dec 03 14:19:13 2009 +0100
@@ -14,9 +14,16 @@
chapter {* Isabelle Essentials *}
text {*
+ \begin{flushright}
+ {\em One man's obfuscation is another man's abstraction.} \\[1ex]
+ Frank Ch.~Eigler on the Linux Kernel Mailing List,\\
+ 24~Nov.~2009
+ \end{flushright}
+
+ \medskip
Isabelle is build around a few central ideas. One central idea is the
LCF-approach to theorem proving where there is a small trusted core and
- everything else is build on top of this trusted core
+ everything else is built on top of this trusted core
\cite{GordonMilnerWadsworth79}. The fundamental data
structures involved in this core are certified terms and certified types,
as well as theorems.