diff -r f1743ce9dbf1 -r 2656354c7544 ProgTutorial/Essential.thy --- 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.