Re: [isabelle] How to use latex commands inside proof?

On Fri, 12 Sep 2014, W. Douglas Maurer wrote:

> I have also had problems with comments starting with -- which is why I > always use comments contained in (* and *) (this has always worked for > me, including backslashes).

There is a common misunderstanding of "formal comments" within the Isar language versus "source comments" (* *) that suppress certain parts of the input for the document preparation system. The latter corresponds to % in latex, i.e. you use it mainly to "comment-out" material that is not part of the proper document.

I need to be more specific as to the problems I have had with the double-hyphen comments. I was debugging a larger lemma, and in the process of doing this, I typed:
lemma induc2a: "(x::nat)=1 ==> x+x+x=3" by auto
and this worked. So then I tried putting a comment on the end, like this:
lemma induc2a: "(x::nat)=1 ==> x+x+x=3" by auto -- this works!
and I got a squiggly line under the exclamation point at the end, and the message "Outer syntax error: command expected, but keyword ! was found".

This is because the argument to the formal comment "--" needs to be an atomic item in Isar token syntax. As already shown in earlier examples it can be done

  -- {* like this *}


  -- ‹like this›

which uses the new cartouche syntax of Isabelle2014.

In general, you have two possibilities:

  (1) read the isar-ref manual carefully what the syntax really is

  (2) read existing examples and applications carefully how things are
      usually done.

If you just make a meta-comment to yourself, without any formal significance, the (* *) form might be actually what you want, but that is relatively rare.


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