Re: [isabelle] How do I make notation work only on the constant instead of on the type as well?
On Wed, 16 Mar 2011, Rafal Kolanski wrote:
I'm on Isabelle 2009-2, and I'm stuck with the following problem. I have
a structure whose constructor name is the same as its type. For
presentation in LaTeX I'm using a notation hack which makes constants a
different font than normal isabelle text.
Here's the problem. I define notation as:
typ "('a, 'p, blah_C) ptr_t"
and: term "blah_C x y z" prints: "moo x y z" :: moo
Why does output notation pick up on the type, when I'm not using a type
translation? How do I specify I want the constant blah_C as the target
of my notation and not the type?
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and