--- a/doc-src/IsarImplementation/implementation.tex Thu Jul 06 15:21:33 2006 +0200
+++ b/doc-src/IsarImplementation/implementation.tex Thu Jul 06 16:49:36 2006 +0200
@@ -16,7 +16,7 @@
\isadroptag{theory}
\title{\includegraphics[scale=0.5]{isabelle_isar}
\\[4ex] The Isabelle/Isar Implementation}
-\author{\emph{Makarius M. M. Wenzel}}
+\author{\emph{Makarius Wenzel}}
\makeglossary
\makeindex
@@ -39,7 +39,7 @@
{\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
+ 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.}