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

On Thu, 28 Aug 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.

So the problem of (* *) within actual Isabelle documents is not just a conceptual mismatch, but also odd extra white space in unexpected situations, instead of informative text.

As a rule of thumb, a proper Isabelle document contains little (* *), but interjects the formally-checked and pretty-printed Isar source with commands for semi-formal pieces as follows:

  section ‹Foo›

  subsection ‹Bar›

  text ‹Blah blah blub.›

  lemma "a = a" .. -- ‹Foo bar blah.›

The "isar-ref" and "system" manuals tell more about Isabelle document preparation.


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