Re: [isabelle] rigorous axiomatic geometry proof in Isabelle

Tim, that sounds great!  Please send me anything you like privately.
I'd love to look at your code.  But if you know the answer to the
question I just posted, please post the answer on the list.  How in
Isabelle do we define models of some FOL axioms and then prove
theorems about the models?  And feel free to post an answer to my
geometry questions too!  How in Tarski's axioms do you prove Hilbert's
full Pasch axiom and angle construction axiom from Tarksi's?


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