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
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