equal
deleted
inserted
replaced
9 \addtolength{\voffset}{-2cm} |
9 \addtolength{\voffset}{-2cm} |
10 \addtolength{\textheight}{4cm} |
10 \addtolength{\textheight}{4cm} |
11 |
11 |
12 \renewcommand{\thesection}{\arabic{section}} |
12 \renewcommand{\thesection}{\arabic{section}} |
13 \renewcommand{\isamarkupheader}[1]{\newpage\markright{Theory~\isabellecontext}\section{#1}} |
13 \renewcommand{\isamarkupheader}[1]{\newpage\markright{Theory~\isabellecontext}\section{#1}} |
14 |
14 \newcommand{\mJava}{$\mu$Java} |
15 |
15 |
16 \begin{document} |
16 \begin{document} |
17 |
17 |
18 \title{$\mu$Java} |
18 \title{\mJava} |
19 \author{Gerwin Klein \\ Tobias Nipkow \\ David von Oheimb \\ Cornelia Pusch} |
19 \author{Gerwin Klein \\ Tobias Nipkow \\ David von Oheimb \\ Cornelia Pusch} |
20 \maketitle |
20 \maketitle |
21 |
21 |
22 \begin{abstract} |
22 \begin{abstract} |
23 This formal development defines Micro Java, a small fragment of the |
23 This formal development defines \mJava, a small fragment of the |
24 programming language Java (essentially just classes), together with a |
24 programming language Java (with essentially just classes), together with a |
25 corresponding virtual machine and a specification of its bytecode verifier. |
25 corresponding virtual machine and a specification of its bytecode verifier. |
26 It is shown that Micro Java and the given specification of the bytecode |
26 It is shown that \mJava and the given specification of the bytecode |
27 verifier are type safe. |
27 verifier are type-safe. |
28 \end{abstract} |
28 \end{abstract} |
29 |
29 |
30 \tableofcontents |
30 \tableofcontents |
31 \parindent 0pt \parskip 0.5ex |
31 \parindent 0pt \parskip 0.5ex |
32 |
32 |