Re: [isabelle] Single-line comments in Isar

Unless it is a single identifier, you need to quote the comment, either with ".." or (more robust!!) with {*..*}.


Peter Vincent Homeier wrote:
I am studying Isar, and have a simple question about comments.

In "Structured Proofs in Isar/HOL" by Nipkow, on page 5 there is what
appears to be a single-line comment, which I approximate below in

  proof (rule conjE[OF AB])  -- conjE[OF AB]: ([[A; B]] ==> ?R) ==> ?R

Also, in "Isar -- A Generic Interpretive Approach to Readable Formal
Proof Documents" by Wenzel, in section 4.4 on page 14 appears

  Formal Comments of the form "-- <text>" may be associated with any
Isar language element.  The comment <text> may contain any text, which
may again contain references to formal entities (terms, formulas,
theores etc.).

But when I have tried using these "-- <text>" comments with
Isabelle2005, I get the response

*** Outer syntax error: end of input expected,
*** but keyword "[" was found

Are these single-line comments still supported?  If so, how are they
properly used?


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