diff -r 760a567f1609 -r aedf7b01c6e4 src/Doc/ProgProve/Isar.thy
--- a/src/Doc/ProgProve/Isar.thy	Thu Jul 11 13:33:20 2013 +0200
+++ b/src/Doc/ProgProve/Isar.thy	Thu Jul 11 21:34:37 2013 +0200
@@ -1048,6 +1048,34 @@
 the induction hypotheses are instead found under the name @{text hyps}, like for the simpler
 @{text induct} method.
 \end{warn}
+
+\section*{Exercises}
+
+\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}
+
+\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$. For example, the production $S
+\to a S b$ can be viewed as the implication @{prop"S w \<Longrightarrow> S (a # w @ [b])"}
+where @{text a} and @{text b} are constructors of some datatype of terminal
+symbols: \isacom{datatype} @{text"tsymbs = a | b | \<dots>"}
+
+Define the two grammars
+\[
+\begin{array}{r@ {\quad}c@ {\quad}l}
+S &\to& \varepsilon \quad\mid\quad a~S~b \quad\mid\quad S~S \\
+T &\to& \varepsilon \quad\mid\quad T~a~T~b
+\end{array}
+\]
+($\varepsilon$ is the empty word)
+as two inductive predicates and prove @{prop"S w \<longleftrightarrow> T w"}.
+\end{exercise}
+
 *}
 (*
 lemma "\<not> ev(Suc(Suc(Suc 0)))"