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



Hi Ondrej,

Thanks. It also works in my real case.

Best,
Andreas

On 24/07/14 20:25, Ondřej Kunčar wrote:
Was addressed in b590fcd03a4a. Andreas, please, double-check that it works for you. I
tested it only on your minimal example.

Ondrej

On 07/22/2014 11:49 PM, Ondřej Kunčar wrote:
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.