Re: [isabelle] Isabelle2014-RC0: lift_definition ignores no_code



On 07/22/2014 10:30 PM, Florian Haftmann wrote:
With Isabelle2014-RC1 approaching, I would like to revive this questions
as I am also, so to speak, a »stake holder« of the theories where this
problem occurs.

So,
a) is this a deliberate change? (There is however no entry containing
»lift« in the NEWS).
b) if not, what shall we do about it?  Someone must put on the helmet
and dig into to investigate,

I'll do it.





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