--- 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}