--- a/doc-src/Exercises/2002/a6/generated/a6.tex Fri Apr 29 18:13:28 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{a{\isadigit{6}}}%
-\isamarkupfalse%
-%
-\isamarkupsubsection{The towers of Hanoi%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-In section \ref{psv2000hanoi} we introduced the towers of Hanoi and
-defined a function \isa{moves} to generate the moves to solve the
-puzzle. Now it is time to show that \isa{moves} is correct. This
-means that
-\begin{itemize}
-\item when executing the list of moves, the result is indeed the
-intended one, i.e.\ all disks are moved from one peg to another, and
-\item all of the moves are legal, i.e.\ never place a larger disk
-on top of a smaller one.
-\end{itemize}
-Hint: this is a nontrivial undertaking. The complexity of your proofs
-will depend crucially on your choice of model and you may have to
-revise your model as you proceed with the proof.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isamarkupfalse%
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End: