*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] How do I make notation work only on the constant instead of on the type as well?*From*: Rafal Kolanski <rafalk at cse.unsw.edu.au>*Date*: Thu, 17 Mar 2011 01:25:29 +1100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <alpine.LNX.1.10.1103161451110.15406@atbroy100.informatik.tu-muenchen.de>*References*: <4D80A402.3000104@cse.unsw.edu.au> <alpine.LNX.1.10.1103161335040.14064@atbroy100.informatik.tu-muenchen.de> <4D80B1E6.4010405@cse.unsw.edu.au> <alpine.LNX.1.10.1103161451110.15406@atbroy100.informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.2.14) Gecko/20110223 Thunderbird/3.1.8

On 17/03/11 00:57, Makarius wrote:

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 (!)"

Thank you Makarius! Rafal Kolanski.

**References**:**[isabelle] How do I make notation work only on the constant instead of on the type as well?***From:*Rafal Kolanski

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

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

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

- Previous by Date: Re: [isabelle] How do I make notation work only on the constant instead of on the type as well?
- Next by Date: Re: [isabelle] Theorem-proving for a Bayesian model compiler
- Previous by Thread: Re: [isabelle] How do I make notation work only on the constant instead of on the type as well?
- Next by Thread: [isabelle] CFP: ICTSS-11 in Paris
- Cl-isabelle-users March 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list