# HG changeset patch
# User oheimb
# Date 969035810 -7200
# Node ID ed35be80285df28d037d162b33ca50d543baca3d
# Parent  6bff6a162d80010053698540b63534d0eb0d359a
added mJava macro

diff -r 6bff6a162d80 -r ed35be80285d src/HOL/MicroJava/document/root.tex
--- 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}