*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 13:38:08 +0100 (CET)*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <4D80A402.3000104@cse.unsw.edu.au>*References*: <4D80A402.3000104@cse.unsw.edu.au>*User-agent*: Alpine 1.10 (LNX 962 2008-03-14)

On Wed, 16 Mar 2011, Rafal Kolanski wrote:

I'm on Isabelle 2009-2, and I'm stuck with the following problem. I havea structure whose constructor name is the same as its type. Forpresentation in LaTeX I'm using a notation hack which makes constants adifferent font than normal isabelle text.Here's the problem. I define notation as: notation (output) blah_C ("moo") then: typ "('a, 'p, blah_C) ptr_t" prints: ('a,'p,moo) ptr_t and: term "blah_C x y z" prints: "moo x y z" :: mooWhy does output notation pick up on the type, when I'm not using a typetranslation? How do I specify I want the constant blah_C as the targetof my notation and not the type?

So the above should work properly, if this is really Isabelle2009-2. Makarius

**Follow-Ups**:

**References**:

- Previous by Date: Re: [isabelle] Theorem-proving for a Bayesian model compiler
- 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: [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