*To*: Rafal Kolanski <rafalk at cse.unsw.edu.au>*Subject*: Re: [isabelle] How do I make notation work only on the constant instead of on the type as well?*From*: Makarius <makarius at sketis.net>*Date*: Wed, 16 Mar 2011 14:57:20 +0100 (CET)*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <4D80B1E6.4010405@cse.unsw.edu.au>*References*: <4D80A402.3000104@cse.unsw.edu.au> <alpine.LNX.1.10.1103161335040.14064@atbroy100.informatik.tu-muenchen.de> <4D80B1E6.4010405@cse.unsw.edu.au>*User-agent*: Alpine 1.10 (LNX 962 2008-03-14)

On Wed, 16 Mar 2011, Rafal Kolanski wrote:

I meant Isabelle 2009-1. Do you know of any way of brute-forcing theissue on this version?

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.

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

**Follow-Ups**:

**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

- 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] How do I make notation work only on the constant instead of on the type as well?
- 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: Re: [isabelle] How do I make notation work only on the constant instead of on the type as well?
- 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