Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] quote in mixfix annotation


view this post on Zulip 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

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

view this post on Zulip 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: Oct 25 2021 at 19:15 UTC