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 meant Isabelle 2009-1. Do you know of any way of brute-forcing the issue on this version?

Isabelle2009-1 does provide authentic syntax, but not for certain older packages. So it depends what you mean by the following:

I have a structure whose constructor name is the same as its type.

Is this a HOL datatype?  This is probably the most delicate situation.

For output of plain constructor terms, you can use 'abbreviation' with its own notation (the const is authentic here). It does not work for patterns, though. For example:

datatype blah_C = blah_C

abbreviation (output)
  blah_C_syntax ("moo")
  where "blah_C_syntax == blah_C"

typ blah_C  -- "blah_C"
term blah_C  -- "moo"
term "case x of blah_C => y"  -- "blah_C (!)"


	Makarius





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