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_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
