Re: [isabelle] Minor bug in output from "locale" with notation



On 25/05/18 00:28, Eugene W. Stark wrote:
> 
>   locale L =
>   fixes X :: "'x ⇒ 'x ⇒ 'x" (infixr "⋅" 55)
> 
> 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.

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




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