[isabelle] Problem with translations
in previous versions of Isabelle, the following worked:
"_SCHEME6 N D P" == (prop)"N == (_AXIOM3 D P)"
(where _SCHEME is a paraphrasing roughly defined by:
"_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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and