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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and