[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 <makarius at sketis.net 
>> <mailto:makarius at 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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5156 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180206/2909a714/attachment.bin>