*To*: Bill Richter <richter at math.northwestern.edu>*Subject*: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle*From*: "Tim (McKenzie) Makarios" <tjm1983 at gmail.com>*Date*: Fri, 14 Sep 2012 11:48:01 +1200*Cc*: makarius at sketis.net, cl-isabelle-users at lists.cam.ac.uk*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:15.0) Gecko/20120827 Thunderbird/15.0

On 02/05/12 14:07, Bill Richter wrote: > I'm concerned about lemma A1, which just restates the > axiom A1. I do something like that in my Mizar code, and I was really > hoping it wouldn't be necessary in Isabelle. Maybe I don't know what > lemma A1 is for. It's lemma A1', not just A1. Its purpose is to turn axiom A1, which is a sentence, into something more useful, with schematic variables that can be instantiated. I think I figured out later that A1 [rule_format] would achieve the same thing, without having to prove lemma A1' separately. Sorry; it's taken me an awfully long time to get around to this, and perhaps it's already been answered, but perhaps my answer will be useful for someone. Tim <><

**Attachment:
signature.asc**

- Previous by Date: Re: [isabelle] Parallel proofs issue, potentially in subst method (also, backtraces)
- Next by Date: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Previous by Thread: Re: [isabelle] Comparing pairs
- Next by Thread: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Cl-isabelle-users September 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