--- a/src/Doc/ProgProve/Logic.thy Thu Nov 07 16:08:19 2013 +1100
+++ b/src/Doc/ProgProve/Logic.thy Fri Nov 08 08:59:54 2013 +0100
@@ -817,6 +817,14 @@
\endexercise
\begin{exercise}
+Analogous to @{const star}, give an inductive definition of the @{text n}-fold iteration
+of a relation @{text r}: @{term "iter r n x y"} should hold if there are @{text x\<^sub>0}, \dots, @{text x\<^sub>n}
+such that @{prop"x = x\<^sub>0"}, @{prop"x\<^sub>n = y"} and @{text"r x\<^bsub>i\<^esub> x\<^bsub>i+1\<^esub>"} for
+all @{prop"i < n"}. Correct and prove the following claim:
+@{prop"star r x y \<Longrightarrow> iter r n x y"}.
+\end{exercise}
+
+\begin{exercise}
A context-free grammar can be seen as an inductive definition where each
nonterminal $A$ is an inductively defined predicate on lists of terminal
symbols: $A(w)$ mans that $w$ is in the language generated by $A$.