--- a/src/HOL/MicroJava/document/root.tex Fri Sep 15 18:14:30 2000 +0200
+++ b/src/HOL/MicroJava/document/root.tex Fri Sep 15 18:36:50 2000 +0200
@@ -20,10 +20,10 @@
\maketitle
\begin{abstract}
- This formal development defines \mJava, a small fragment of the
+ This formal development defines {\mJava}, a small fragment of the
programming language Java (with essentially just classes), together with a
corresponding virtual machine and a specification of its bytecode verifier.
- It is shown that \mJava and the given specification of the bytecode
+ It is shown that {\mJava} and the given specification of the bytecode
verifier are type-safe.
\end{abstract}