\documentclass[10pt,a4paper]{article}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage{sectsty}
\usepackage{xpatch}
\usepackage{csquotes}
\usepackage{upquote}
\usepackage{isabelle,isabellesym}
\usepackage{amssymb}
\usepackage{xcolor}
\usepackage{listings}

\makeatletter
\xpatchcmd{\@maketitle}
{\@title}
{%\vspace{-2.45\baselineskip}
\bfseries\@title\vspace{.25\baselineskip}}
{}{}
\makeatother

\makeatletter
\providecommand{\institute}[1]{%
  \apptocmd{\@author}{\end{tabular}%
  \vspace{.5\baselineskip}\par
  \begin{tabular}[t]{c}
  #1}{}{}
}
\makeatother

\newcommand{\email}[1]{%
  \texttt{\href{mailto:#1}{\color{black}{#1}}}%
}

\pretocmd{\tableofcontents}{\sectionfont{\Huge}}{}{}
%\let\clearpage\relax
\apptocmd{\tableofcontents}{\sectionfont{\Large}}{}{}

% further packages required for unusual symbols (see also
% isabellesym.sty), use only when needed

%\usepackage{amssymb}
  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
  %\<triangleq>, \<yen>, \<lozenge>

%\usepackage{eurosym}
  %for \<euro>

%\usepackage[only,bigsqcap,bigparallel,fatsemi,interleave,sslash]{stmaryrd}
  %for \<Sqinter>, \<Parallel>, \<Zsemi>, \<Parallel>, \<sslash>

%\usepackage{eufrak}
  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)

%\usepackage{textcomp}
  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
  %\<currency>

% this should be the last package used
\usepackage{pdfsetup}

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}

% for uniform font size
%\renewcommand{\isastyle}{\isastyleminor}

\definecolor{mygreen}{rgb}{0,0.6,0}
\definecolor{mygray}{rgb}{0.5,0.5,0.5}
\definecolor{mymauve}{rgb}{0.58,0,0.82}

\lstset{
  language=OCL,                 % the language of the code
  backgroundcolor=\color{white},   % choose the background color; you must add \usepackage{color} or \usepackage{xcolor}; should come as last argument
  basicstyle=\small\ttfamily,        % the size of the fonts that are used for the code
  breakatwhitespace=false,         % sets if automatic breaks should only happen at whitespace
  breaklines=false,                 % sets automatic line breaking
  captionpos=b,                    % sets the caption-position to bottom
  commentstyle=\color{mygreen},    % comment style
  deletekeywords={...},            % if you want to delete keywords from the given language
  escapeinside={(*@}{@*)},          % if you want to add LaTeX within your code
  extendedchars=true,              % lets you use non-ASCII characters; for 8-bits encodings only, does not work with UTF-8
  frame=single,	                   % adds a frame around the code
  keepspaces=true,                 % keeps spaces in text, useful for keeping indentation of code (possibly needs columns=flexible)
  keywordstyle=\color{mymauve},       % keyword style
  %numbers=left,                    % where to put the line-numbers; possible values are (none, left, right)
  %numbersep=5pt,                   % how far the line-numbers are from the code
  numberstyle=\tiny\color{mygray}, % the style that is used for the line-numbers
  rulecolor=\color{black},         % if not set, the frame-color may be changed on line-breaks within not-black text (e.g. comments (green here))
  showspaces=false,                % show spaces everywhere adding particular underscores; it overrides 'showstringspaces'
  showstringspaces=false,          % underline spaces within strings only
  showtabs=false,                  % show tabs within strings adding particular underscores
  stepnumber=2,                    % the step between two line-numbers. If it's 1, each line will be numbered
  stringstyle=\color{mymauve},     % string literal style
  tabsize=2,	                   % sets default tabsize to 2 spaces
  title=\lstname,                   % show the filename of files included with \lstinputlisting; also try caption instead of title
  texcl=true
}

\lstdefinelanguage{myOCL}{%
  language=OCL,
  morekeywords={let, in, forAll, ->}            % if you want to add more keywords to the set
}

\newcommand{\mapping}[2]{\(#1\)-to-\(#2\)}


\begin{document}

\title{Formalization of a Brake System}
\author{Michael Kirsten and Terru St{\"{u}}binger}
\institute{%
Ludwig-Maximilians-Universit{\"{a}}t~(LMU) M{\"{u}}nchen, Munich, Germany\\
Karlsruhe Institute of Technology (KIT), Karlsruhe, Germany\\
\email{michael.kirsten@ifi.lmu.de}, \email{stuebinger@kit.edu}}
\maketitle

\begin{abstract}
Isabelle formalizations of consistency specifications for a brake system case study in view-based software engineering.
\end{abstract}

\tableofcontents

% sane default for proof documents
\parindent 0pt\parskip 0.5ex

% generated text of all theories
\input{session}

% optional bibliography
%\bibliographystyle{abbrv}
%\bibliography{root}

\end{document}
