# HG changeset patch
# User nipkow
# Date 1384584353 -3600
# Node ID 0e1c576bbc190d2d7ac5e07a8d25c3a08748080b
# Parent  4a655e62ad34d2fad0ea25081a1da6dae5c90c26
tuned

diff -r 4a655e62ad34 -r 0e1c576bbc19 src/Doc/ProgProve/Bool_nat_list.thy
--- 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:
diff -r 4a655e62ad34 -r 0e1c576bbc19 src/Doc/ProgProve/Isar.thy
--- 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
diff -r 4a655e62ad34 -r 0e1c576bbc19 src/Doc/ProgProve/Logic.thy
--- 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
diff -r 4a655e62ad34 -r 0e1c576bbc19 src/Doc/ProgProve/Types_and_funs.thy
--- 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