
diff -r ff6787d730d5 -r 260090b54ef9 doc-src/Exercises/exercises.tex
--- a/doc-src/Exercises/exercises.tex	Fri Apr 29 18:13:28 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,135 +0,0 @@
-\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, Farhad Mehta, 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}
-\aufgabe{2003}{a1}{a1}
-\aufgabe{2003}{a2}{a2}
-\aufgabe{2003}{a3}{a3}
-\aufgabe{2003}{a5}{a5}
-\aufgabe{2003}{a6}{a6}
-
-%--------------------------------------------
-\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}




