doc-src/TutorialI/Overview/LNCS/document/root.tex

--- a/doc-src/TutorialI/Overview/LNCS/document/root.tex	Wed Jul 31 16:10:24 2002 +0200
+++ b/doc-src/TutorialI/Overview/LNCS/document/root.tex	Wed Jul 31 17:42:38 2002 +0200
@@ -11,7 +11,8 @@
 \begin{document}
 
 \title{A Compact Overview of Isabelle/HOL}
-\author{Tobias Nipkow}
+\author{Tobias Nipkow\\Institut f{\"u}r Informatik, TU M{\"u}nchen\\
+ \small\url{http://www.in.tum.de/~nipkow/}}
 \date{}
 \maketitle
 
@@ -28,6 +29,16 @@
 \subsection{An Introductory Theory}
 \input{FP0.tex}
 
+\begin{exercise}
+Define a datatype of binary trees and a function \isa{mirror}
+that mirrors a binary tree by swapping subtrees recursively. Prove
+\isa{mirror(mirror t) = t}.
+
+Define a function \isa{flatten} that flattens a tree into a list
+by traversing it in infix order. Prove
+\isa{flatten(mirror t) = rev(flatten t)}.
+\end{exercise}
+
 \subsection{More Constructs}
 \input{FP1.tex}