Re: [isabelle] Isabelle2014-RC0: lift_definition ignores no_code
Was addressed in b590fcd03a4a. Andreas, please, double-check that it
works for you. I tested it only on your minimal example.
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
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