Email Gateway (Aug 18 2022 at 11:24): Email Gateway (Aug 18 2022 at 11:24):From: Peter Vincent Homeier <palantir@trustworthytools.com>
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
Email Gateway (Aug 18 2022 at 11:24):From: Tobias Nipkow <nipkow@in.tum.de>
Unless it is a single identifier, you need to quote the comment, either
with ".." or (more robust!!) with {..}.
Regards
Tobias
Peter Vincent Homeier wrote:
Last updated: May 03 2024 at 12:27 UTC