src/Doc/Prog_Prove/Types_and_funs.thy
changeset 58860 fee7cfa69c50
parent 58620 7435b6a3f72e
child 64862 2baa926a958d
     1.1 --- a/src/Doc/Prog_Prove/Types_and_funs.thy	Sat Nov 01 11:40:55 2014 +0100
     1.2 +++ b/src/Doc/Prog_Prove/Types_and_funs.thy	Sat Nov 01 14:20:38 2014 +0100
     1.3 @@ -298,8 +298,8 @@
     1.4  \end{quote}
     1.5  Of course one cannot do this naively: @{prop"itrev xs ys = rev xs"} is
     1.6  just not true.  The correct generalization is
     1.7 -*};
     1.8 -(*<*)oops;(*>*)
     1.9 +*}
    1.10 +(*<*)oops(*>*)
    1.11  lemma "itrev xs ys = rev xs @ ys"
    1.12  (*<*)apply(induction xs, auto)(*>*)
    1.13  txt{*