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.