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.}