*To*: "Tim (McKenzie) Makarios" <tjm1983 at gmail.com>*Subject*: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle*From*: Bill Richter <richter at math.northwestern.edu>*Date*: Sun, 29 Apr 2012 23:02:40 -0500*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4F9E0AB4.5060402@gmail.com> (tjm1983@gmail.com)*References*: <201204282058.q3SKw9NF008441@poisson.math.northwestern.edu> <4F9E0AB4.5060402@gmail.com>

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? -- Best, Bill

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

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Tim (McKenzie) Makarios

- Previous by Date: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Next by Date: Re: [isabelle] Proof General of Isabelle/jEdit
- Previous by Thread: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Next by Thread: [isabelle] Using Isar on Induction
- Cl-isabelle-users April 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