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

Lawrence Paulson lp15 at cam.ac.uk
Mon May 29 13:21:01 CEST 2023

Looks reasonable to me!


> 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.

More information about the isabelle-dev mailing list