--- a/src/Doc/Prog_Prove/Types_and_funs.thy Thu Aug 07 12:17:41 2014 +0200
+++ b/src/Doc/Prog_Prove/Types_and_funs.thy Fri Aug 08 08:26:32 2014 +0200
@@ -389,7 +389,7 @@
\begin{array}{r@ {}c@ {}l@ {\quad}l}
@{text"(0 + Suc 0"} & \leq & @{text"Suc 0 + x)"} & \stackrel{(1)}{=} \\
@{text"(Suc 0"} & \leq & @{text"Suc 0 + x)"} & \stackrel{(2)}{=} \\
-@{text"(Suc 0"} & \leq & @{text"Suc (0 + x)"} & \stackrel{(3)}{=} \\
+@{text"(Suc 0"} & \leq & @{text"Suc (0 + x))"} & \stackrel{(3)}{=} \\
@{text"(0"} & \leq & @{text"0 + x)"} & \stackrel{(4)}{=} \\[1ex]
& @{const True}
\end{array}