[isabelle-dev] Proposal to add a new \<notapprox> symbol and corresponding glyph to the Isabelle font

[Lawrence Paulson]

Looks reasonable to me!

Larry

> On 28 May 2023, at 22:00, Martin Desharnais <martin.desharnais at posteo.de> wrote:
> 
> I propose to add a glyph for its negation "≉" (U+2249 Not Almost Equal To). For the corresponding symbol name, I propose \<notapprox> similarly to how we have \<noteq> and \<notin>.
> 
> Note that I cannot write ¬(x≈y) instead, as my use case is to define abbreviations for positive and negative literals in a formalization of first-order logic with equality.