
diff -r 33124a9f5e31 -r 553d48cac687 doc-src/IsarImplementation/implementation.tex
--- 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.}




