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}