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

[Martin Desharnais]

Dear Makarius, dear Isabelle developers,

the Isabelle font contains a glyph for the unicode character "≈" (U+2248 
Almost Equal To) usable through the symbol \<approx>.

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.

datatype 'a literal = Pos 'a | Neg 'a

abbreviation pos_eq (infix "≈" 50) where
   "t1 ≈ t2 ≡ Pos (Upair t1 t2)"

abbreviation neg_eq (infix "≉" 50) where
   "t1 ≉ t2 ≡ Neg (Upair t1 t2)"

Regards,
Martin Desharnais