[isabelle] quote in mixfix annotation



>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)))) ^^^^^^^^^^^^

theory Biegelinie_Test
  imports Complex_Main
begin

consts
(*
  both, 1 and 2 NOT outcommented causes the error "Ambiguous input" below;
  either 1 or 2 OUTCOMMENTED shows the term structure at the bottom.
*)
(*1*)M'_b  :: "real => real" ("M'_b")   (* Biegemoment                *)(**)
(*2*)M'_b' :: "real => real" ("M'_b' ") (* Ableitung des Biegemoments *)(**)
     V     :: "real => real"            (* Querkraft                  *)
     y''   :: "real => real"            (* 2.Ableitung der Biegeline  *)
     EI    :: "real"                    (* Biegesteifigkeit           *)
                                                 
axiomatization where
  Moment_Querkraft: "M_b' x = V x" and
  Neigung_Moment:   "y'' x = -M_b x/ EI"
(*
Ambiguous input\<^here> 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))))
Ambiguous input
2 terms are type correct:
  ((y'' x) = ((- (M_b x)) / EI))
  ((y'' x) = ((- (M_b x)) / EI))
Failed to parse prop
*)

ML \<open>
val prop = Thm.prop_of @{thm "Moment_Querkraft"}
(*1 OUTCOMMENTED: (Var (("M_b'", 0), "real \<Rightarrow> ?'a")         !!!!!NOT Const
  2 OUTCOMMENTED: (Var (("M_b'", 0), "real \<Rightarrow> real")        !!!!!NOT Const
*)
\<close> ML \<open>
val prop = Thm.prop_of @{thm "Neigung_Moment"}
(*1 OUTCOMMENTED: (Const ("Biegelinie_Test.M'_b'", "real \<Rightarrow> real")   !!!!!
  2 OUTCOMMENTED: (Const ("Biegelinie_Test.M'_b", "real \<Rightarrow> real")   !!!!!NO '
*)
\<close>
end


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