Re: [isabelle] Quotients of nominal types



Am 12.08.2013 10:25, schrieb Dmitriy Traytel:
Am 12.08.2013 09:38, schrieb Christian Urban:
There is no way, I think, to
lift/transfer theorems by names (on the non-ML-level).
I think the transferred attribute is supposed to do just that.
Oh, I see now that my reply applies to the development version only (e.g. Isabelle/0cd62cb233e0). In Isabelle2013 this attribute is implemented by legacy_transfer (i.e. not working with Lifting/Transfer).

Dmitriy





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