Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] quote in mixfix annotation

Email Gateway (Oct 06 2020 at 08:05):

From: Walther Neuper <walther.neuper@jku.at>
From Isabelle2019 to Isabelle2020 there is a change in handling quotes
in mixfix annotations (PS1).

Now, when updating our project to the new Isabelle version, this change
breaks definitions of constants, which are named according to standard
notation in structural engineering:   M⇩b   and   M⇩b'

Although I do not (yet) lookup the symbol tables directly, I see from an
error message (PS2), that the parser fails with the two identifiers. The
respective cut-down theory is attached. I couldn't make a clue from the
isar-ref manual, so my question:

Is there a possibility to continue the standard notations for   M⇩b  
and for   M⇩b'  , or should we let these from now on?

Walther

PS1: NEWS

• Mixfix annotations may use "' " (single quote followed by space) to
  separate delimiters (as documented in the isar-ref manual), without
  requiring an auxiliary empty block. A literal single quote needs to be
  escaped properly. Minor INCOMPATIBILITY.

PS2:

Ambiguous input⌂ produces 2 parse trees:

("\<^const>HOL.Trueprop"

("\<^const>HOL.eq" ("_applC" ("_position" y'') ("_position" x))

("\<^const>Fields.inverse_class.inverse_divide"
("\<^const>Groups.uminus_class.uminus" ("_applC"
("\<^const>Biegelinie_Test.M'_b") ("_position" x)))

("_position" EI))))

("\<^const>HOL.Trueprop"

("\<^const>HOL.eq" ("_applC" ("_position" y'') ("_position" x))

("\<^const>Fields.inverse_class.inverse_divide"
("\<^const>Groups.uminus_class.uminus" ("_applC"
("\<^const>Biegelinie_Test.M'_b'") ("_position" x)))

("_position" EI)))) ^^^^^^^^^^^^
Biegelinie_Test.thy

Email Gateway (Jan 02 2021 at 10:11):

From: Makarius <makarius@sketis.net>
(This rather old thread appears to be still open.)

You merely need to escape the single quote within mixfix, i.e. using "b'' "
instead of former "b' ".

Makarius

Last updated: Jan 04 2025 at 20:18 UTC