[isabelle-dev] Typing problem in autogenerated axiom

[Andreas Schropp]

Dominique Unruh wrote:
>> Most of our problems stem from HOL and Pure sharing a function space,
>> whereas ZF has its own set theoretic one, which is of course very different
>> from the Pure one. I solved this by a stratification of types into HOL/Pure
>> parts, and carrying this stratification schematically through the whole
>> translation process, which works because proof constants are only
>> schematically polymorphic.
>>     
>
> Yes, the nice thing about Coq is that it is almost an exact superset
> of what is available in HOL (at least when we use the various optional
> Coq-axioms like excluded-middle and extensionality-of-equality).
>   

Hmm, what about typedefs? I thought they are a peculiarity of HOL and 
its set-theoretic model. What do they correspond to in Coq?

>
>
>
> So overall, I think the best approach for me is approach B, because it
> should work well and be compatible with the current plans for the
> Isabelle kernel.
>   

Yes, it sounds like that.

> Best,
> Dominique
>