<commit_before>
\documentclass[11pt,a4paper]{article}
\usepackage{latexsym,isabelle,isabellesym,pdfsetup}

\urlstyle{rm}
\pagestyle{myheadings}

\addtolength{\hoffset}{-1,5cm}
\addtolength{\textwidth}{4cm}
\addtolength{\voffset}{-2cm}
\addtolength{\textheight}{4cm}

%subsection instead of section to make the toc readable
\renewcommand{\thesubsection}{\arabic{subsection}}
\renewcommand{\isamarkupheader}[1]{\newpage\markright{Theory~\isabellecontext}\subsection{#1}}

%remove spaces from the isabelle environment (trivlist makes them too large)
\renewenvironment{isabelle}
{\begin{isabellebody}}
{\end{isabellebody}}

\newcommand{\mJava}{$\mu$Java}

%remove clutter from the toc
\setcounter{secnumdepth}{2}
\setcounter{tocdepth}{2}

\begin{document}

\title{\mJava}
\author{<NAME> \\ <NAME> \\ <NAME> \\ <NAME>}
\maketitle

\begin{abstract}\noindent
  This formal development defines {\mJava}, a small fragment of the
  programming language Java (with essentially just classes), together with a
  corresponding virtual machine, a specification of its bytecode verifier
  and a lightweight bytecode verifier.<commit_msg>tuned<commit_after>
\documentclass[11pt,a4paper]{article}
\usepackage{latexsym,isabelle,isabellesym,pdfsetup}

\urlstyle{rm}
\pagestyle{myheadings}

\addtolength{\hoffset}{-1,5cm}
\addtolength{\textwidth}{4cm}
\addtolength{\voffset}{-2cm}
\addtolength{\textheight}{4cm}

%subsection instead of section to make the toc readable
\renewcommand{\thesubsection}{\arabic{subsection}}
\renewcommand{\isamarkupheader}[1]{\newpage\markright{Theory~\isabellecontext}\subsection{#1}}
\renewcommand{\isamarkupsection}[1]{\subsubsection{#1}}

%remove spaces from the isabelle environment (trivlist makes them too large)
\renewenvironment{isabelle}
{\begin{isabellebody}}
{\end{isabellebody}}

\newcommand{\mJava}{$\mu$Java}

%remove clutter from the toc
\setcounter{secnumdepth}{3}
\setcounter{tocdepth}{2}

\begin{document}

\title{\mJava}
\author{<NAME> \\ <NAME> \\ <NAME> \\ <NAME>}
\maketitle

\begin{abstract}\noindent
  This formal development defines {\mJava}, a small fragment of the
  programming language Java (with essentially just classes), together with a
  corresponding virtual machine, a specification of its bytecode verifier
  and a lightweight bytecode verifier.
{'fraction_non_alphanumeric': 0.13624454148471615, 'fraction_numerical': 0.011353711790393014, 'mean_word_length': 6.561056105610561, 'pattern_counts': {'":': 0, '<': 11, '<?xml version=': 0, '>': 11, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1063138', 'n_tokens_mistral': 760, 'n_tokens_neox': 748, 'n_words': 168}