--- a/src/Doc/ProgProve/Logic.thy Sat Oct 26 13:01:41 2013 +0200
+++ b/src/Doc/ProgProve/Logic.thy Sat Oct 26 23:06:40 2013 +0200
@@ -780,10 +780,10 @@
\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}
-instruction on a stack of size less than two. Define an inductive predicate
+Consider the stack machine from Chapter~3
+and recall the concept of \concept{stack underflow}
+from Exercise~\ref{exe:stack-underflow}.
+Define an inductive predicate
@{text "ok :: nat \<Rightarrow> instr list \<Rightarrow> nat \<Rightarrow> bool"}
such that @{text "ok n is n'"} means that with any initial stack of length
@{text n} the instructions @{text "is"} can be executed