| changeset 58519 | 7d85162e8520 |
| parent 58504 | 5f88c142676d |
| child 58521 | b70e93c05efe |
--- 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;(*>*)