Re: [isabelle] Operator clash for $

> 2. Disable the "$" notation completely outside the FPS theory, or put it
> in a locale that has to be interpreted every time one wants to use the
> notation. On the down side, one still runs into problems when one wants
> to use the $ notation for FPSs but has Multivariate_Analysis loaded as
> well. I guess one could put both of them in locales, but I don't know if
> we want that.

Note that starting from a59801b7f125 bundles have become a convenient
mechanism to organize modularized syntax.  The Â$Â notation would be a
nice candidate to demonstrate that.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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