[isabelle-dev] Some thoughts on mixfix syntax partially applied [was: NEWS]

[Makarius]

On Tue, 22 Sep 2015, Tobias Nipkow wrote:

> The "op" noation is idiosyncratic, but there are examples (not in 
> individual formulae) where I find some such notation convenient. I would 
> welcome Haskell's "(+)", but that has a problem with "(*)". Unless we 
> can make that notation work, I don't think we profit much by a change. 
> Hence I am inclined to leave things as they are.

"(*)" does not work, because it is in conflict with "(* comment *)" in 
inner syntax.  I have recently encountered a situation where it would have 
been better to replace inner comments by "-- ‹comment›", as known in outer 
syntax, but the double-minus was in conflict with some infix operators. 
The next idea was to replace "-- ‹comment›" by "— ‹comment›" with a newly 
introduced Isabelle symbol for the mdash.

So many clouds of dust, caused by trying to clean up obscure corners ...

At the moment I am also inclined to leave things unchanged.


 	Makarius