# [isabelle] question on "notation"

Hi there,

`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
``use it. 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 that
``constant and the type constructor "set").
`

`My goal was to make the conversion from lists into sets 'implicit' in my
``resulting PDF. Any suggestions, how to achieve this?
`
cheers
chris

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*