Re: [isabelle] Sum of first n integers

Thanks Lars!

On Wed, Oct 21, 2015 at 11:14 AM, Lars Noschinski <noschinl at>

> On 21.10.2015 06:06, Rustom Mody wrote:
> > In paper
> > 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.

Maybe so
But I think I am stuck on something much more preliminary

The example starts with

fixes "n :: nat"
shows "(â i =0.. n . i ) = n â ( n + 1) div 2"

[assuming that's how the quotes should be put

But it looks that Isabelle (or should I be saying Isar?) wants some prefix

theory sum
imports Main

which gives the following at theorem

Outer syntax errorâ: proposition expected,
but keyword (â was found

> 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.

Good to know!


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