Re: [isabelle] rigorous axiomatic geometry proof in Isabelle

>There is, of course, Isabelle/ZF, which does use FOL and the ZF axioms

Is there a deep reason to code geometry axioms inside HOL? It seems to me it would be more natural to build Tarski geometry logic based on FOL, in the similar way like ZF logic is built on FOL. 

Library of Formalized Mathematics for Isabelle/Isar (ZF Logic)

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