Re: [isabelle] How to use latex commands inside proof?
- To: "W. Douglas Maurer" <maurer at gwu.edu>
- Subject: Re: [isabelle] How to use latex commands inside proof?
- From: Makarius <makarius at sketis.net>
- Date: Wed, 10 Sep 2014 20:10:41 +0200 (CEST)
- Cc: cl-isabelle-users at lists.cam.ac.uk
- In-reply-to: <email@example.com>
- References: <firstname.lastname@example.org>
- User-agent: Alpine 2.00 (LNX 1167 2008-08-23)
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:
text ‹Blah blah blub.›
lemma "a = a" .. -- ‹Foo bar blah.›
The "isar-ref" and "system" manuals tell more about Isabelle document
This archive was generated by a fusion of
Pipermail (Mailman edition) and