[isabelle-dev] Proposal to add a new \<notapprox> symbol and corresponding glyph to the Isabelle font
martin.desharnais at posteo.de
Sun May 28 23:00:33 CEST 2023
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)"
More information about the isabelle-dev