[isabelle] ZF theories with HOL



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



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