Re: [isabelle] Quotients of nominal types
Am 12.08.2013 10:25, schrieb Dmitriy Traytel:
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).
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and