doc-src/Exercises/exercises.tex

Added PSV 2003/2004

\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,\\ 
  Martin Strecker, 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
\section{2003/2004}
\aufgabe{0304}{a1}{a1}
\aufgabe{0304}{a2}{a2}
\aufgabe{0304}{a3}{a3}
\aufgabe{0304}{a4}{a4}
\aufgabe{0304}{a5}{a5}

%--------------------------------------------
\newpage

\bibliographystyle{abbrv}
\bibliography{exercises}

\end{document}