Re: [isabelle] Separation of Isabelle/Pure and Isabelle/HOL and typedef [concerning: Isabelle Foundation & Certification]



On 22 Sep 2015, at 15:26, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
> 
> * move typedef to Pure (which seems just to be wrong, although I have no
> example at hand for a valid Pure model that would be invalidated by that).

I think this could work, using a meta-level predicate of course. It could closely resemble the version in HOL4. I havenât thought this through, but the other thing it needs is an equality symbol, which we have in the meta-logic.

Whether it would cause significant architectural upheavals is another question. There might be simpler solutions to the problem at hand. I donât have a clear idea of how the circularity check works and whether typedef it could feed into it.

Larry



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