Re: [isabelle] How do I make notation work only on the constant instead of on the type as well?




On 16/03/11 23:38, Makarius wrote:
That is a feature of all Isabelle versions until Isabelle2009-1. In
Isabelle2009-2 the syntax becaume fully "authentic" after many years of
reforming the system (see also the NEWS for Isabelle2009-2).

So the above should work properly, if this is really Isabelle2009-2.

Actually, I apologise, that was a typo due to being tired and stressed. I meant Isabelle 2009-1. Do you know of any way of brute-forcing the issue on this version? I'm low on time and I don't care about elegance, especially if the problem no longer exists on 2009-2 and afterwards.

Hats off to whoever solved this in subsequent versions. I didn't even notice the problem was there until it hit me over the head.

Sincerely,

Rafal Kolanski.





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