*To*: Christian Sternagel <c-sterna at jaist.ac.jp>*Subject*: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle*From*: Bill Richter <richter at math.northwestern.edu>*Date*: Tue, 1 May 2012 23:09:07 -0500*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4FA0A63C.7030904@jaist.ac.jp> (message from Christian Sternagel on Wed, 02 May 2012 12:13:00 +0900)*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> <4FA0A63C.7030904@jaist.ac.jp>

Jeremy, if you or anyone else wants to talk about Euclid off-line, I'd be happy to talk. As I try to explain in my paper, I love the Elements http://www.math.northwestern.edu/~richter/hilbert.pdf It's very creative and forms the basis of non-Euclidean geometry. Thanks, Chris, that's very helpful. I'll look for the red wavy error lines in jedit. I'll look at /src/HOL/ex/. I've looked at tutorial.pdf, but I'll look again, and isar-overview.pdf sounds good. Thanks for explaining simp, blast etc, although I don't really know what you mean. Is there somewhere an FOL example, with a long (perhaps indigestible) single step "rule" method proof, which is shortened with simp, and then shortened even more with blast & auto? (In courses it is often done that students are only allowed to use certain rules in order to proof a statement, since the automatic tools would outright solve many typical examples.) Wow! Can you point me to any of these courses? That sounds like what I need to know. As I posted earlier, I'm mostly trying to cite some good code for my geometry paper above (which I'll then submit). I don't have to write the code myself, although I did http://www.math.northwestern.edu/~richter/RichterTarskiMizar.tar Examples of real classroom situations where students hand in Isabelle proofs would be fantastic! Dunno about Europe, but US public schools are really gungho about computer applications. -- Best, Bill

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

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

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Christian Sternagel

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