\<^bsub> .. \<^esub>
\input{style}
\usepackage{graphicx}
\usepackage[colorlinks,hyperindex]{hyperref}
\newcommand{\aufgabe}[3]{
\input{#1/#2/generated/#3}
%\newpage
}
\title{Isabelle/HOL Exercises}
\date{\today}
\author{Gertrud Bauer, Gerwin Klein, Tobias Nipkow,\\ Michael Wahler, Markus Wenzel}
\begin{document}
\maketitle
This document presents a collection of exercises for getting
acquainted with the proof assistant
Isabelle/HOL~\cite{isabelle-tutorial}. The exercises come out of an
annual Isabelle/HOL course taught at the Technical University of
Munich. They are arranged in chronological order, and in each year in
ascending order of difficulty.
\tableofcontents
%--------------------------------------------
\newpage
\section{2000}
\aufgabe{2000}{a1}{Snoc}
\aufgabe{2000}{a1}{Arithmetic}
\aufgabe{2000}{a1}{Hanoi}
%\aufgabe{2000}{a2}{BDT}
%\aufgabe{2000}{a2}{OBDT}
%\aufgabe{2000}{a3}{NaturalDeduction}
%\aufgabe{2000}{a3}{HoareLogic}
%\aufgabe{2000}{a4}{CTLexample}
%\aufgabe{2000}{a5}{Unix}
%\section{L{\"o}sungen}
%\aufgabe{2000}{l1}{Snoc}
%\aufgabe{2000}{l1}{Arithmetic}
%\aufgabe{2000}{l1}{Hanoi}
%\aufgabe{2000}{l2}{BDT}
%\aufgabe{2000}{l2}{OBDT}
%\aufgabe{2000}{l3}{NaturalDeduction}
%\aufgabe{2000}{l3}{HoareLogic}
%\aufgabe{2000}{l4}{CTLexample}
%\aufgabe{2000}{l5}{Unix}
%--------------------------------------------
\newpage
\section{2001}
\aufgabe{2001}{a1}{Aufgabe1}
\aufgabe{2001}{a2}{Aufgabe2}
\aufgabe{2001}{a3}{Trie1}
\aufgabe{2001}{a3}{Trie2}
\aufgabe{2001}{a3}{Trie3}
%\aufgabe{2001}{a4}{Aufgabe4}
\aufgabe{2001}{a5}{Aufgabe5}
%\aufgabe{2001}{a5}{PL}
%\aufgabe{2001}{a6}{Aufgabe6}
%\section{L{\"o}sungen}
%\aufgabe{2001}{l1}{Aufgabe1}
%\aufgabe{2001}{l2}{Loesung2}
%\aufgabe{2001}{l3}{Trie1}
%\aufgabe{2001}{l3}{Trie2}
%\aufgabe{2001}{l3}{Trie3}
%\aufgabe{2001}{l4}{Loesung4}
%\aufgabe{2001}{l5}{Loesung5}
%\aufgabe{2001}{l5}{PL}
%\aufgabe{2001}{l6}{Loesung6}
%--------------------------------------------
\newpage
\section{2002}
\aufgabe{2002}{a1}{a1}
\aufgabe{2002}{a2}{a2}
\aufgabe{2002}{a3}{a3}
%\aufgabe{2002}{a4}{a4}
\aufgabe{2002}{a5}{a5}
\aufgabe{2002}{a6}{a6}
%\aufgabe{2002}{a7}{a7}
%\newpage
%\section{L{\"o}sungen}
%\aufgabe{2002}{l1}{l1}
%\aufgabe{2002}{l2}{l2}
%\aufgabe{2002}{l3}{l3}
%\aufgabe{2002}{l4}{l4}
%\aufgabe{2002}{l5}{l5}
%\aufgabe{2002}{l6}{l6}
%\aufgabe{2002}{l7}{ABP}
%\newpage
%\part{Anhang}
%\section{Zu 2000}
%\aufgabe{2000}{a4}{GfpLfp}
%\aufgabe{2000}{a4}{CTL}
%\aufgabe{2000}{a5}{Env}
%\section{Zu 2001}
%\aufgabe{2001}{a6}{Hoare}
\newpage
\bibliographystyle{abbrv}
\bibliography{exercises}
\end{document}