doc-src/Exercises/exercises.tex

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/exercises.tex	Thu Dec 05 17:12:07 2002 +0100
@@ -0,0 +1,112 @@
+\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}