
diff -r a4c82a9ff7d8 -r dbc19b772f5b doc-src/IsarImplementation/implementation.tex
--- a/doc-src/IsarImplementation/implementation.tex	Sat Mar 04 21:10:12 2006 +0100
+++ b/doc-src/IsarImplementation/implementation.tex	Sat Mar 04 21:39:08 2006 +0100
@@ -33,6 +33,31 @@
   architecture, and provide clues on implementing user extensions.
 \end{abstract}
 
+\vspace*{2.5cm}
+\begin{quote}
+  
+  {\small\em Isabelle was not designed; it evolved.  Not everyone
+    likes this idea.  Specification experts rightly abhor
+    trial-and-error programming.  They suggest that no one should
+    write a program without First writing a complete formal
+    specification. But university departments are not software houses.
+    Programs like Isabelle are not products: when they have served
+    their purpose, they are discarded.}
+  
+  Lawrence C. Paulson, ``Isabelle: The Next 700 Theorem Provers''
+
+  \vspace*{1cm}
+  
+  {\small\em As I did 20 years ago, I still fervently believe that the
+    only way to make software secure, reliable, and fast is to make it
+    small.  Fight Features.}
+  
+  Andrew S. Tanenbaum
+
+\end{quote}
+
+\thispagestyle{empty}\clearpage
+
 \pagenumbering{roman} \tableofcontents \clearfirst
 
 \input{intro.tex}
@@ -43,20 +68,6 @@
 \input{Thy/document/locale.tex}
 \input{Thy/document/integration.tex}
 
-% Isabelle was not designed; it evolved.
-% Not everyone likes this idea. Specification experts rightly abhor trial-and-error programming.
-% They suggest that no one should write a program without First writing a complete
-% formal specification. But university departments are not software houses. Programs like
-% Isabelle are not products: when they have served their purpose, they are discarded.
-%
-% L.C. Paulson, ``Isabelle: The Next 700 Theorem Provers''
-
-% As I did 20 years ago, I still fervently believe that the only way to
-% make software secure, reliable, and fast is to make it small. Fight
-% Features.
-%
-% Andrew S. Tanenbaum
-
 \appendix
 \input{Thy/document/ML.tex}
 




