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}