diff -r 0a06b51ffa56 -r 4d3a481fc48e src/Doc/ProgProve/Logic.thy
--- a/src/Doc/ProgProve/Logic.thy	Thu Oct 24 19:43:21 2013 +0200
+++ b/src/Doc/ProgProve/Logic.thy	Fri Oct 25 16:20:54 2013 +0200
@@ -769,6 +769,17 @@
 \subsection{Exercises}
 
 \begin{exercise}
+In \autoref{sec:AExp} we defined a recursive evaluation function
+@{text "aval :: aexp \<Rightarrow> state \<Rightarrow> val"}.
+Define an inductive evaluation predicate
+@{text "aval_rel :: aexp \<Rightarrow> state \<Rightarrow> val \<Rightarrow> bool"}
+and prove that it agrees with the recursive function:
+@{prop "aval_rel a s v \<Longrightarrow> aval a s = v"}, 
+@{prop "aval a s = v \<Longrightarrow> aval_rel a s v"} and thus
+\noquotes{@{prop [source] "aval_rel a s v \<longleftrightarrow> aval a s = v"}}.
+\end{exercise}
+
+\begin{exercise}
 Consider the stack machine from \autoref{sec:aexp_comp}.
 A \concept{stack underflow} occurs when executing an instruction
 on a stack containing too few values, e.g., executing an @{text ADD}