ProgTutorial/Essential.thy
changeset 410 2656354c7544
parent 409 f1743ce9dbf1
child 412 73f716b9201a
--- 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.