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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and