[isabelle] Attributes for unnamed facts in obtains



Hi all,

the Isar command obtains works without "where" when only facts, but no new variables are obtained, although I have not found a proper syntax documentation for that in the Isabelle/Iar reference manual.

The following three examples work as expected:

from `A & B` obtain foo [intro]: "A" and bar [simp]: "B" by(rule conjE)
from `A & B` obtain foo: "A" and [simp]: "B" by(rule conjE)
from `A & B` obtain [intro]: "A" and "B" by(rule conjE)
from `A & B` obtain [intro]: "A" and [simp]: "B" by(rule conjE)
from `A & B` obtain "A" and "" [simp]: "B" by(rule conjE)

However, if the first fact is unnamed and without attributes, and only an attribute is given for the second fact (like in the next example), the parser produces a syntax error:

from `A & B` obtain "A" and [simp]: "B" by(rule conjE)

*** Outer syntax error: name declaration expected,
*** but keyword [ was found

Is there any specific reason for this?

Best regards,
Andreas

--
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Gebäude 50.41, Raum 023
76131 Karlsruhe

Telefon: +49 721 608-8352
Fax: +49 721 608-8457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Großforschungszentrum in der Helmholtz-Gemeinschaft





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