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