Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] ZF theories with HOL

Email Gateway (Aug 22 2022 at 13:38):

From: Omar Jasim <oajasim1@sheffield.ac.uk>
Dear list,

I need to define a set of pairs with a relation like : <a,b>:f which f is a
function of a "b=f(a)" . I found this in func.thy under ZF which define
functions, function space and many other stuff. The problem is I need to
use HOL as well and I couldn't becuase they are different platform. So is
there such away to connect between ZF and HOL? or I should redefine this
func theory in HOL which too hard. I found that there is HOL-ZF logic
session but I'm not sure if it include definitions like in func theory in
ZF.

Regards

Omar

Last updated: May 06 2024 at 12:29 UTC