# HG changeset patch
# User nipkow
# Date 1412282025 -7200
# Node ID 7d85162e852006affac5ea3877fa9c48eef7d228
# Parent  07901e99565c56dc6eb07f49018bf8ece4d9f448
tuned

diff -r 07901e99565c -r 7d85162e8520 src/Doc/Prog_Prove/Types_and_funs.thy
--- a/src/Doc/Prog_Prove/Types_and_funs.thy	Thu Oct 02 20:04:00 2014 +0200
+++ b/src/Doc/Prog_Prove/Types_and_funs.thy	Thu Oct 02 22:33:45 2014 +0200
@@ -296,7 +296,7 @@
 \begin{quote}
 \emph{Generalize goals for induction by replacing constants by variables.}
 \end{quote}
-Of course one cannot do this na\"{\i}vely: @{prop"itrev xs ys = rev xs"} is
+Of course one cannot do this naively: @{prop"itrev xs ys = rev xs"} is
 just not true.  The correct generalization is
 *};
 (*<*)oops;(*>*)