Re: [isabelle] rigorous axiomatic geometry proof in Isabelle



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
Description: OpenPGP digital signature



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