--- a/src/Doc/ProgProve/Isar.thy Fri Nov 08 19:03:14 2013 +0100
+++ b/src/Doc/ProgProve/Isar.thy Fri Nov 08 21:40:07 2013 +0100
@@ -1081,8 +1081,7 @@
\exercise
-Give a structured proof of @{prop "ev(Suc(Suc n)) \<Longrightarrow> ev n"}
-by rule inversion:
+Give a structured proof by rule inversion:
*}
lemma assumes a: "ev(Suc(Suc n))" shows "ev n"
@@ -1098,6 +1097,13 @@
\end{exercise}
\begin{exercise}
+Recall predicate @{text star} from \autoref{sec:star} and @{text iter}
+from Exercise~\ref{exe:iter}. Prove @{prop "iter r n x y \<Longrightarrow> star r x y"}
+in a structured style, do not just sledgehammer each case of the
+required induction.
+\end{exercise}
+
+\begin{exercise}
Define a recursive function @{text "elems ::"} @{typ"'a list \<Rightarrow> 'a set"}
and prove @{prop "x : elems xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> elems ys"}.
\end{exercise}