Re: [isabelle-dev] NEWS: formal comments

On 06.02.2018 17:31, Tobias Nipkow wrote: This concerns only the inner syntax, where comments are rare. We should not give up the outer (* *) comments for something less convenient. Informal outer comments are not going to disappear. That means that users who don't have a formal meaning of

Re: [isabelle-dev] NEWS: formal comments

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

Re: [isabelle-dev] NEWS: formal comments

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 wrote: > > * Old-style inner comments (* ... *) within the term language are legacy > and will be

[isabelle-dev] Code check failed for SML on lxbroy10

Dear isabelle-dev, I noticed that currently (isabelle:ed0a7090167d, AFP:26f074817c9a) AFP/Native_Word fails to build on lxbroy10 (with ML_system_64=true): *** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure *** At command

[isabelle-dev] 25th Automated Reasoning Workshop (ARW 2018), University of Cambridge, 12-13 April 2018

25th AUTOMATED REASONING WORKSHOP 2018 Cambridge, 12-13 April 2018 http://www.cl.cam.ac.uk/events/arw2018/ CALL FOR ABSTRACTS AND STUDENT TRAVEL GRANT APPLICATIONS GENERAL INFORMATION The 25th Automated Reasoning Workshop (ARW 2018) will take place at the University of Cambridge on 12-13