--- a/src/Doc/Prog_Prove/Isar.thy Tue Aug 25 10:28:30 2015 +0200
+++ b/src/Doc/Prog_Prove/Isar.thy Tue Aug 25 10:41:12 2015 +0200
@@ -1122,10 +1122,10 @@
\begin{exercise}
Extend Exercise~\ref{exe:cfg} with a function that checks if some
\mbox{@{text "alpha list"}} is a balanced
-string of parentheses. More precisely, define a recursive function
+string of parentheses. More precisely, define a \mbox{recursive} function
@{text "balanced :: nat \<Rightarrow> alpha list \<Rightarrow> bool"} such that @{term"balanced n w"}
-is true iff (informally) @{text"S (a\<^sup>n @ w)"}. Formally, prove
-@{prop "balanced n w \<longleftrightarrow> S (replicate n a)"} where
+is true iff (informally) @{text"S (a\<^sup>n @ w)"}. Formally, prove that
+@{prop "balanced n w \<longleftrightarrow> S (replicate n a @ w)"} where
@{const replicate} @{text"::"} @{typ"nat \<Rightarrow> 'a \<Rightarrow> 'a list"} is predefined
and @{term"replicate n x"} yields the list @{text"[x, \<dots>, x]"} of length @{text n}.
\end{exercise}