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

     2.1 --- a/src/Doc/ProgProve/Logic.thy	Fri Nov 08 19:03:14 2013 +0100
     2.2 +++ b/src/Doc/ProgProve/Logic.thy	Fri Nov 08 21:40:07 2013 +0100
     2.3 @@ -816,7 +816,7 @@
     2.4  if the assumption about the inductive predicate is not the first assumption.
     2.5  \endexercise
     2.6  
     2.7 -\begin{exercise}
     2.8 +\begin{exercise}\label{exe:iter}
     2.9  Analogous to @{const star}, give an inductive definition of the @{text n}-fold iteration
    2.10  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}
    2.11  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