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.

Cheers,
	Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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