Re: [isabelle] Isabelle2019-RC2: Experience report



On 19/05/2019 19:33, Makarius wrote:
> On 14/05/2019 13:46, Peter Lammich wrote:
>>   * The NEWS file does not specify any replacement for old style inner
>> comments (* *). The entry for Isabelle-2018 says to use \comment or
>> \cancel. However, content of \comment is interpreted as latex text,
>> causing trouble with unknown antiquotations when e.g. trying to comment
>> out "{1,2}@{a,b}". Moreover, \cancel used to occur in "striked out"
>> style in Latex output, at least when used in outer syntax. Is this also
>> the case for inner-syntax \cancel? 
> 
> Old style inner comments were not really well-defined, and treated
> differently from outer comments (which are like % in LaTeX).
> 
> The purpose of the reform of formal comments was to make it all work
> uniformly, e.g. see the included example.

Here is again the Test.thy with its document.pdf -- the makers of
Thunderbird seem to believe in Physics more than Mathematics: when
updating an attached file in the file-system, its updated version is
sent out.


	Makarius

theory Test
  imports Main
begin

section \<open>Formal comments in outer syntax\<close>

term x \<comment> \<open>informal text\<close>
term x \<comment> \<open>\<open>formal @{text}\<close>\<close>
term x \<comment> \<open>\<^verbatim>\<open>verbatim @{text}\<close>\<close>

term x \<^cancel>\<open>cancel\<close>


section \<open>Formal comments in inner syntax\<close>

term \<open>x \<comment> \<open>informal text\<close>\<close>
term \<open>x \<comment> \<open>\<open>formal @{text}\<close>\<close>\<close>
term \<open>x \<comment> \<open>\<^verbatim>\<open>verbatim @{text}\<close>\<close>\<close>

term \<open>x \<^cancel>\<open>cancel\<close>\<close>

end

Attachment: document.pdf
Description: Adobe PDF document



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.