[opentheory-users] Embedding Z (or other ZFC fragments) in HOL

[Roger Jones]

On 7 Jan 2015 16:56, Freek Wiedijk <freek at cs.ru.nl> wrote:
>

> This is an engineered version of what you wrote after this: 
> that you can have functions that ignore their argument, 
> and just return information about the type of the argument 
>

The underlying phenomenon necessitated  constraints on definitions introduced into HOL in about 1988 and further discussed in Rob Arthan's recent HOLS conference paper.

Roger Jones