src/Doc/Prog_Prove/Types_and_funs.thy

--- a/src/Doc/Prog_Prove/Types_and_funs.thy	Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Prog_Prove/Types_and_funs.thy	Sat Nov 01 14:20:38 2014 +0100
@@ -298,8 +298,8 @@
 \end{quote}
 Of course one cannot do this naively: @{prop"itrev xs ys = rev xs"} is
 just not true.  The correct generalization is
-*};
-(*<*)oops;(*>*)
+*}
+(*<*)oops(*>*)
 lemma "itrev xs ys = rev xs @ ys"
 (*<*)apply(induction xs, auto)(*>*)
 txt{*