--- a/doc-src/IsarImplementation/implementation.tex Tue Jan 03 11:57:33 2006 +0100
+++ b/doc-src/IsarImplementation/implementation.tex Tue Jan 03 13:59:55 2006 +0100
@@ -49,7 +49,13 @@
% 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
+% 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}