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