Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] Proposal to add a new \<notapprox> symbol ...

view this post on Zulip Email Gateway (May 28 2023 at 21:00):

From: 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)"

Martin Desharnais

isabelle-dev mailing list

view this post on Zulip Email Gateway (May 29 2023 at 11:21):

From: Lawrence Paulson <>
Looks reasonable to me!


isabelle-dev mailing list

Last updated: Mar 04 2024 at 10:08 UTC