[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.