From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
In Isabelle 2017, if I load the theory:
theory Barf
imports Main
begin
locale L =
fixes X :: "'x ⇒ 'x ⇒ 'x" (infixr "⋅" 55)
end
and then put the mouse over the locale definition, I see the following
in the output window:
locale
L
fixes X :: "'x ⇒ 'x ⇒ 'x" (infixl "⋅" 55)
That is, it seems to output the fixity incorrectly.
From: Makarius <makarius@sketis.net>
The output is indeed incorrect. There are a few more oddities in the
formatting and the defaults for other mixfix annotations.
I will improve this for the coming release -- presumably published in
August 2018.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC