*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle*From*: Christian Sternagel <c-sterna at jaist.ac.jp>*Date*: Wed, 02 May 2012 12:13:00 +0900*In-reply-to*: <201205020207.q4227VoC013147@poisson.math.northwestern.edu>*References*: <201204282058.q3SKw9NF008441@poisson.math.northwestern.edu> <CAFP4q14YwNi6RksUOkGNGWYYzkNi3ca92FH4kYW19kJeOBcT2Q@mail.gmail.com> <alpine.LNX.2.00.1204301125350.6594@macbroy21.informatik.tu-muenchen.de> <201205020207.q4227VoC013147@poisson.math.northwestern.edu>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:12.0) Gecko/20120424 Thunderbird/12.0

Dear Bill, On 05/02/2012 11:07 AM, Bill Richter wrote:

I ran the executable ./Isabelle and up popped jedit. I pasted in Isabelle code from Tim's master's thesis into Scratch.thy. There's extensive jedit help on the Help menu, but I couldn't figure out how to compile my buffer.

Concerning some of the points you mentioned:

hope this helps, chris

**Follow-Ups**:**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Bill Richter

**References**:**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Bill Richter

- Previous by Date: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Next by Date: [isabelle] jEdit (unexpected?) behavior
- Previous by Thread: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Next by Thread: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Cl-isabelle-users May 2012 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