*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*: Wed, 16 Mar 2011 23:49:42 +1100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <alpine.LNX.1.10.1103161335040.14064@atbroy100.informatik.tu-muenchen.de>*References*: <4D80A402.3000104@cse.unsw.edu.au> <alpine.LNX.1.10.1103161335040.14064@atbroy100.informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.2.13) Gecko/20101208 Thunderbird/3.1.7

On 16/03/11 23:38, Makarius wrote:

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.

Sincerely, Rafal Kolanski.

**Follow-Ups**:

**References**:

- 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