src/Doc/ProgProve/Logic.thy
changeset 54436 0e1c576bbc19
parent 54292 ce4a17b2e373
child 54839 327f282799db
--- 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