--- a/src/Doc/ProgProve/Types_and_funs.thy Thu Nov 14 20:55:09 2013 +0100
+++ b/src/Doc/ProgProve/Types_and_funs.thy Sat Nov 16 07:45:53 2013 +0100
@@ -201,7 +201,7 @@
except in its name, and is applicable independently of @{text f}.
-\subsection{Exercises}
+\subsection*{Exercises}
\begin{exercise}
Starting from the type @{text "'a tree"} defined in the text, define
@@ -336,7 +336,7 @@
those that change in recursive calls.
-\subsection{Exercises}
+\subsection*{Exercises}
\begin{exercise}
Write a tail-recursive variant of the @{text add} function on @{typ nat}:
@@ -523,7 +523,7 @@
Method @{text auto} can be modified in exactly the same way.
-\subsection{Exercises}
+\subsection*{Exercises}
\exercise\label{exe:tree0}
Define a datatype @{text tree0} of binary tree skeletons which do not store