[isabelle] Single-line comments in Isar



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
ascii:

  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?

Peter
-- 
"In Your majesty ride prosperously
because of truth, humility, and righteousness;
and Your right hand shall teach You awesome things." (Psalm 45:4)





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