# HG changeset patch
# User nipkow
# Date 1382821600 -7200
# Node ID 9d239afc1a903b9bf133e87894006c8a38e23c70
# Parent  16723c8344069fa547e6774c4d90da54d40cfa9d
more exercises

diff -r 16723c834406 -r 9d239afc1a90 src/Doc/ProgProve/Logic.thy
--- 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