# HG changeset patch
# User wenzelm
# Date 1152197376 -7200
# Node ID 553d48cac687949c580dcda22d960bd91755085c
# Parent  33124a9f5e31d71ec3e55184715c1a11944b9a4f
tuned;

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.}
diff -r 33124a9f5e31 -r 553d48cac687 doc-src/IsarImplementation/style.sty
--- a/doc-src/IsarImplementation/style.sty	Thu Jul 06 15:21:33 2006 +0200
+++ b/doc-src/IsarImplementation/style.sty	Thu Jul 06 16:49:36 2006 +0200
@@ -53,6 +53,7 @@
 \newcommand{\isasymCONSTS}{\isakeyword{consts}}
 \newcommand{\isasymDEFS}{\isakeyword{defs}}
 \newcommand{\isasymTHEOREM}{\isakeyword{theorem}}
+\newcommand{\isasymDEFINITION}{\isakeyword{definition}}
 
 \isabellestyle{it}