Email Gateway (Aug 18 2022 at 09:38): Email Gateway (Aug 18 2022 at 09:38):From: Burkhart Wolff <bwolff@inf.ethz.ch>
Dear all,
in previous versions of Isabelle, the following worked:
translations
"_SCHEME6 N D P" == (prop)"N == (_AXIOM3 D P)"
(where _SCHEME is a paraphrasing roughly defined by:
syntax
"_SCHEME6":: " ... " (" ... " )
)
According to the Isar-Reference Manual, this syntax still
exists, allowing to specify optionally the non-terminal
for the lhs or rhs of the translation.
Unfortunately, the syntactic category "prop" is no longer recognized
by the Isar Parser (it works for "logic" or so, but this
leads to other obvious problems ...) According to the Isabelle
Reference Manual, prop is still the syntactic category for
expressions like A ==> B or A == B.
Any ideas for a remedy or a work-around?
Best,
bu
Email Gateway (Aug 18 2022 at 09:38):From: Makarius <makarius@sketis.net>
Just use quotes around "prop". The name/nameref category happens to allow
non-quoted identifiers as well, but these occur so often that it is easy
to forget the more general form of explicitly quoted names.
Makarius
Last updated: May 03 2024 at 08:18 UTC