*To*: Harry Butterworth <heb1001 at gmail.com>*Subject*: Re: [isabelle] Sum of first n integers*From*: Rustom Mody <rustompmody at gmail.com>*Date*: Wed, 21 Oct 2015 14:55:52 +0530*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAMUwPhyNFCG97H4OEiMJ3202VycZ-1h_YC5M=7CGBznCN2Gnag@mail.gmail.com>*References*: <CAJ+TeofX7WZJ+ubA1dvXs=MNQmGDdr2KzchDHe8bY6p=D6NKSQ@mail.gmail.com> <56272622.1000400@in.tum.de> <CAJ+Teofw1L-vUOe0zU+etRrAopQp+rxUKYmM8FmHG3=-4EbRQg@mail.gmail.com> <CAMUwPhyNFCG97H4OEiMJ3202VycZ-1h_YC5M=7CGBznCN2Gnag@mail.gmail.com>

Thanks Harry On Wed, Oct 21, 2015 at 2:11 PM, Harry Butterworth <heb1001 at gmail.com> wrote: > Your star is the wrong star character. Maybe you have cut and pasted from > a pdf document. That doesn't work. > > Yeah I started with https://www.lri.fr/~wenzel/Isabelle_Paris_2014/slides.pdf And was looking for a source/thy version of that... > With the version below... > > theory sum > imports Main > begin > > theorem > fixes n::nat > shows "(â i =0.. n . i ) = n * ( n + 1) div 2" > > ...I get the output > > proof (prove): depth 0 > > goal (1 subgoal): > 1. â{0..n} = n * (n + 1) div 2 > > Harry > My current thy file is attached. It has about a dozen 'red-marks' :-)

**Attachment:
sum.thy**

**Follow-Ups**:**Re: [isabelle] Sum of first n integers***From:*Harry Butterworth

**References**:**[isabelle] Sum of first n integers***From:*Rustom Mody

**Re: [isabelle] Sum of first n integers***From:*Lars Noschinski

**Re: [isabelle] Sum of first n integers***From:*Rustom Mody

**Re: [isabelle] Sum of first n integers***From:*Harry Butterworth

- Previous by Date: Re: [isabelle] Sum of first n integers
- Next by Date: Re: [isabelle] Sum of first n integers
- Previous by Thread: Re: [isabelle] Sum of first n integers
- Next by Thread: Re: [isabelle] Sum of first n integers
- Cl-isabelle-users October 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list