[isabelle] Transitioning between ZF and HOL



Title: Transitioning between ZF and HOL

I am attempting to develop ring theory in HOL, and at the same time prove that these rings are categorically equivalent to rings founded in Zermelo-Fraenkel set theory.  It has been singularly difficult to find resources that describe the transition between ZF and the typed set theory that one finds in Isabelle, or a more general type theory.  Is there anyone here who could point me to good references?

Thanks,
Robert Lamar



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