# HG changeset patch
# User nipkow
# Date 1407479192 -7200
# Node ID dfebc374bd89270bce67f30faa4b5433da11367b
# Parent  d8bbb97689d3d2235ba51d8005e1d2e538f5a8d8
tuned

diff -r d8bbb97689d3 -r dfebc374bd89 src/Doc/Prog_Prove/Types_and_funs.thy
--- 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}