# Re: [isabelle] Sum of first n integers

On 21.10.2015 06:06, Rustom Mody wrote:
> 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?
It is customary to omit the quotation marks ("), when type-setting
Isabelle theories -- these need to surround every (non-atomic)
expression of the inner syntax.
Refering to slide 24 of the above document, "inner syntax" is everything
printed in cursive, except the proofs (which are proceeded by "by").
For starting, I would recommend to look at "Programming and Proving in
Isabelle/HOL".
>
> Also:
> Spent some hours figuring out what is 'sorry'
> Which manual answers such questions?
The Isabelle/Isar Reference Manual (look at the index at the end of the
document). Be warned that this is a reference manual -- if you do not
already understand how the system works, many explanations are hard to
understand.
> Finally if there is a more noob-list than this one please let me know!
No, this is the right list.
-- Lars

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