1.1 --- a/doc-src/IsarImplementation/implementation.tex	Thu Jul 06 15:21:33 2006 +0200
     1.2 +++ b/doc-src/IsarImplementation/implementation.tex	Thu Jul 06 16:49:36 2006 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4  \isadroptag{theory}
     1.5  \title{\includegraphics[scale=0.5]{isabelle_isar}
     1.6    \\[4ex] The Isabelle/Isar Implementation}
     1.7 -\author{\emph{Makarius M. M. Wenzel}}
     1.8 +\author{\emph{Makarius Wenzel}}
     1.9  
    1.10  \makeglossary
    1.11  \makeindex
    1.12 @@ -39,7 +39,7 @@
    1.13    {\small\em Isabelle was not designed; it evolved.  Not everyone
    1.14      likes this idea.  Specification experts rightly abhor
    1.15      trial-and-error programming.  They suggest that no one should
    1.16 -    write a program without First writing a complete formal
    1.17 +    write a program without first writing a complete formal
    1.18      specification. But university departments are not software houses.
    1.19      Programs like Isabelle are not products: when they have served
    1.20      their purpose, they are discarded.}

     2.1 --- a/doc-src/IsarImplementation/style.sty	Thu Jul 06 15:21:33 2006 +0200
     2.2 +++ b/doc-src/IsarImplementation/style.sty	Thu Jul 06 16:49:36 2006 +0200
     2.3 @@ -53,6 +53,7 @@
     2.4  \newcommand{\isasymCONSTS}{\isakeyword{consts}}
     2.5  \newcommand{\isasymDEFS}{\isakeyword{defs}}
     2.6  \newcommand{\isasymTHEOREM}{\isakeyword{theorem}}
     2.7 +\newcommand{\isasymDEFINITION}{\isakeyword{definition}}
     2.8  
     2.9  \isabellestyle{it}
    2.10