# HG changeset patch
# User oheimb
# Date 969034457 -7200
# Node ID f96d8e02ff1d71d4013e72fe6ea03c733f5736bf
# Parent  09fc8fc746c41a2da78c1f26fadf6c806640f771
added mJava macro

diff -r 09fc8fc746c4 -r f96d8e02ff1d src/HOL/MicroJava/document/root.tex
--- a/src/HOL/MicroJava/document/root.tex	Fri Sep 15 16:55:20 2000 +0200
+++ b/src/HOL/MicroJava/document/root.tex	Fri Sep 15 18:14:17 2000 +0200
@@ -11,20 +11,20 @@
 
 \renewcommand{\thesection}{\arabic{section}}
 \renewcommand{\isamarkupheader}[1]{\newpage\markright{Theory~\isabellecontext}\section{#1}}
-
+\newcommand{\mJava}{$\mu$Java}
 
 \begin{document}
 
-\title{$\mu$Java}
+\title{\mJava}
 \author{Gerwin Klein \\ Tobias Nipkow \\ David von Oheimb \\ Cornelia Pusch}
 \maketitle
 
 \begin{abstract}
-  This formal development defines Micro Java, a small fragment of the
-  programming language Java (essentially just classes), together with a
+  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 Micro Java and the given specification of the bytecode
-  verifier are type safe.
+  It is shown that \mJava and the given specification of the bytecode
+  verifier are type-safe.
 \end{abstract}
 
 \tableofcontents