Re: [isabelle-dev] NEWS: formal comments

[Tobias Nipkow]

This concerns only the inner syntax, where comments are rare. We should not give up the outer (* *) comments for something less convenient.

Tobias

On 06/02/2018 15:13, Lawrence Paulson wrote:

Will there still be a way to comment out random junk? I often work with a mixture of Isabelle and commented-out HOL Light material.

Larry

On 26 Jan 2018, at 20:19, Makarius <makar...@sketis.net <mailto:makar...@sketis.net>> wrote:

* Old-style inner comments (* ... *) within the term language are legacy
and will be discontinued soon: use formal comments "― ‹...›" or "⌦‹...›"
instead.

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

smime.p7s
Description: S/MIME Cryptographic Signature

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev