Email Gateway (May 28 2023 at 21:00): Email Gateway (May 28 2023 at 21:00):From: Martin Desharnais <martin.desharnais@posteo.de>
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
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (May 29 2023 at 11:21):From: Lawrence Paulson <lp15@cam.ac.uk>
Looks reasonable to me!
Larry
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Last updated: Apr 28 2024 at 16:17 UTC