--- a/src/Doc/ProgProve/Bool_nat_list.thy Thu Jul 11 13:33:20 2013 +0200
+++ b/src/Doc/ProgProve/Bool_nat_list.thy Thu Jul 11 21:34:37 2013 +0200
@@ -414,6 +414,19 @@
but underdefined.
\endsem
%
+
+\subsection{Exercises}
+
+\begin{exercise}
+Define your own addition, multiplication, and exponentiation functions on type
+@{typ nat}. Prove as many of the standard equational rules as possible, e.g.\
+associativity, commutativity and distributivity.
+\end{exercise}
+\begin{exercise}
+Define your own sorting function on the predefined lists.
+Prove that the result is sorted and that every element occurs as many times
+in the output as in the input.
+\end{exercise}
*}
(*<*)
end