[isabelle] Product types?

Hi all,

AFAIK, Isabelle's lambda calculus is simply typed, because the types
are built up from base types by means of =>. However, there are
product types in HOL, so how are they encoded?

Thanks for your time.


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