1.1 --- a/doc-src/IsarImplementation/implementation.tex	Sat Mar 04 21:10:12 2006 +0100
     1.2 +++ b/doc-src/IsarImplementation/implementation.tex	Sat Mar 04 21:39:08 2006 +0100
     1.3 @@ -33,6 +33,31 @@
     1.4    architecture, and provide clues on implementing user extensions.
     1.5  \end{abstract}
     1.6  
     1.7 +\vspace*{2.5cm}
     1.8 +\begin{quote}
     1.9 +  
    1.10 +  {\small\em Isabelle was not designed; it evolved.  Not everyone
    1.11 +    likes this idea.  Specification experts rightly abhor
    1.12 +    trial-and-error programming.  They suggest that no one should
    1.13 +    write a program without First writing a complete formal
    1.14 +    specification. But university departments are not software houses.
    1.15 +    Programs like Isabelle are not products: when they have served
    1.16 +    their purpose, they are discarded.}
    1.17 +  
    1.18 +  Lawrence C. Paulson, ``Isabelle: The Next 700 Theorem Provers''
    1.19 +
    1.20 +  \vspace*{1cm}
    1.21 +  
    1.22 +  {\small\em As I did 20 years ago, I still fervently believe that the
    1.23 +    only way to make software secure, reliable, and fast is to make it
    1.24 +    small.  Fight Features.}
    1.25 +  
    1.26 +  Andrew S. Tanenbaum
    1.27 +
    1.28 +\end{quote}
    1.29 +
    1.30 +\thispagestyle{empty}\clearpage
    1.31 +
    1.32  \pagenumbering{roman} \tableofcontents \clearfirst
    1.33  
    1.34  \input{intro.tex}
    1.35 @@ -43,20 +68,6 @@
    1.36  \input{Thy/document/locale.tex}
    1.37  \input{Thy/document/integration.tex}
    1.38  
    1.39 -% Isabelle was not designed; it evolved.
    1.40 -% Not everyone likes this idea. Specification experts rightly abhor trial-and-error programming.
    1.41 -% They suggest that no one should write a program without First writing a complete
    1.42 -% formal specification. But university departments are not software houses. Programs like
    1.43 -% Isabelle are not products: when they have served their purpose, they are discarded.
    1.44 -%
    1.45 -% L.C. Paulson, ``Isabelle: The Next 700 Theorem Provers''
    1.46 -
    1.47 -% As I did 20 years ago, I still fervently believe that the only way to
    1.48 -% make software secure, reliable, and fast is to make it small. Fight
    1.49 -% Features.
    1.50 -%
    1.51 -% Andrew S. Tanenbaum
    1.52 -
    1.53  \appendix
    1.54  \input{Thy/document/ML.tex}
    1.55