HOL4 and HOL Light both support the (sym) syntax to remove concrete syntax fixities. I don't think HOL Light supports comments at this level. HOL4 does, using SML's (* ... *). So, if you want to write the escaped *, you have to use our older syntax for the same (using a $ for "op": $*), or you can just add spaces and write ( *), or ( * ).
Michael > On 6 Oct 2015, at 23:12, Makarius <makar...@sketis.net> wrote: > > 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 ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
