[isabelle] Sum of first n integers

In paper https://www.lri.fr/~wenzel/Isabelle_Paris_2014/slides.pdf
there is the example of sum of first n integers.

Quite stuck at 'outer/inner' syntax errors.
Is there somewhere I can find the full example so that I can study it?

Spent some hours figuring out what is 'sorry'
Which manual answers such questions?

Finally if there is a more noob-list than this one please let me know!

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.