--- a/src/Doc/ProgProve/Bool_nat_list.thy Thu Nov 14 20:55:09 2013 +0100
+++ b/src/Doc/ProgProve/Bool_nat_list.thy Sat Nov 16 07:45:53 2013 +0100
@@ -419,7 +419,7 @@
From now on lists are always the predefined lists.
-\subsection{Exercises}
+\subsection*{Exercises}
\begin{exercise}
Use the \isacom{value} command to evaluate the following expressions:
--- a/src/Doc/ProgProve/Isar.thy Thu Nov 14 20:55:09 2013 +0100
+++ b/src/Doc/ProgProve/Isar.thy Sat Nov 16 07:45:53 2013 +0100
@@ -590,7 +590,7 @@
the fact just proved, in this case the preceding block. In general,
\isacom{note} introduces a new name for one or more facts.
-\subsection{Exercises}
+\subsection*{Exercises}
\exercise
Give a readable, structured proof of the following lemma:
@@ -1077,7 +1077,7 @@
\end{warn}
-\subsection{Exercises}
+\subsection*{Exercises}
\exercise
--- a/src/Doc/ProgProve/Logic.thy Thu Nov 14 20:55:09 2013 +0100
+++ b/src/Doc/ProgProve/Logic.thy Sat Nov 16 07:45:53 2013 +0100
@@ -142,7 +142,7 @@
@{theory Main}.
-\subsection{Exercises}
+\subsection*{Exercises}
\exercise
Start from the data type of binary trees defined earlier:
@@ -788,7 +788,7 @@
transitive closure merely simplifies the form of the induction rule.
-\subsection{Exercises}
+\subsection*{Exercises}
\begin{exercise}
Formalise the following definition of palindromes
--- 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