# HG changeset patch
# User wenzelm
# Date 1265634291 -3600
# Node ID 2ddc7edce107df0410488aae2e20ec4d1cab892d
# Parent  f2f1e50bf65d8190e6f688c4e1ec40212f7d1ae5
more quotes;

diff -r f2f1e50bf65d -r 2ddc7edce107 doc-src/IsarImplementation/implementation.tex
--- a/doc-src/IsarImplementation/implementation.tex	Mon Feb 08 11:13:30 2010 +0100
+++ b/doc-src/IsarImplementation/implementation.tex	Mon Feb 08 14:04:51 2010 +0100
@@ -25,7 +25,7 @@
 
 \begin{document}
 
-\maketitle 
+\maketitle
 
 \begin{abstract}
   We describe the key concepts underlying the Isabelle/Isar
@@ -37,7 +37,7 @@
 
 \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
@@ -45,17 +45,28 @@
     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
 
+  \vspace*{1cm}
+
+  {\small\em One thing that UNIX does not need is more features. It is
+    successful in part because it has a small number of good ideas
+    that work well together. Merely adding features does not make it
+    easier for users to do things --- it just makes the manual
+    thicker. The right solution in the right place is always more
+    effective than haphazard hacking.}
+
+  Rob Pike and Brian W. Kernighan
+
 \end{quote}
 
 \thispagestyle{empty}\clearpage
@@ -89,7 +100,7 @@
 \end{document}
 
 
-%%% Local Variables: 
+%%% Local Variables:
 %%% mode: latex
 %%% TeX-master: t
-%%% End: 
+%%% End: