[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.

John





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