tuned

--- 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;(*>*)