# Re: [isabelle] I can't understand types in set-membership expressions

`Mathematics is most easily formalised using types, with the exception
``of the sort of thing done in set theory: foundational definitions of
``functions, relations, ordinal and cardinal numbers, etc. Set theory is
``therefore rather like assembly language: it is perfect for low level
``developments but otherwise a poor choice if you want to get anything
``done.
`Larry
On 15 Sep 2008, at 23:08, Slawomir Kolodynski wrote:

`Isabelle is mostly used for tasks related to software verification,
``not formalized mathematics. HOL is much better for that.
``A more interesting question is why people choose to do formalized
``mathematics in Isabelle/HOL rather than Isabelle/ZF. For that I
``don't have a good answer.
`

Larry Paulson

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