*To*: Christian Sternagel <christian.sternagel at uibk.ac.at>*Subject*: Re: [isabelle] question on "notation"*From*: Makarius <makarius at sketis.net>*Date*: Mon, 12 Apr 2010 11:03:24 +0200 (CEST)*Cc*: Isabelle List <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <4BC1BAED.2040006@uibk.ac.at>*References*: <4BC1BAED.2040006@uibk.ac.at>*User-agent*: Alpine 1.10 (LNX 962 2008-03-14)

On Sun, 11 Apr 2010, Christian Sternagel wrote:

today I stumbled over some (for me) unexpected behavior of the"notation" command.I'm using the following notation: notation set ("\<^raw:\listset{>_\<^raw:}>") where \newcommand\listset[1]{#1}As soon as I have introduced the notation, however, all "set" types also useit. E.g., @{typ "('a * 'b) set"} is transformed into\isa{\listset{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b}}The same behavior occurs when I'm defining notation for the constant"List.set" instead (and I do not see any connection between thatconstant and the type constructor "set").

My goal was to make the conversion from lists into sets 'implicit' in myresulting PDF. Any suggestions, how to achieve this?

Makarius

**References**:**[isabelle] question on "notation"***From:*Christian Sternagel

- Previous by Date: Re: [isabelle] Quantifying over types
- Next by Date: Re: [isabelle] Quantifying over types
- Previous by Thread: [isabelle] question on "notation"
- Next by Thread: [isabelle] Quantifying over types
- Cl-isabelle-users April 2010 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