From d1c936409ade7d93e67107243cbc0aa55cda7fd5 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Thu, 13 Jul 2023 17:14:42 -0500 Subject: [PATCH] chore: update abbreviations.json (#44) --- data/abbreviations.json | 2 ++ 1 file changed, 2 insertions(+) diff --git a/data/abbreviations.json b/data/abbreviations.json index a839ba7..c41a55d 100644 --- a/data/abbreviations.json +++ b/data/abbreviations.json @@ -429,6 +429,8 @@ "to_s": "→ₛ", "r_s": "→ₛ", "simplefunc": "→ₛ", + "heyting": "⇨", + "himp": "⇨", "covers": "⋖", "covby": "⋖", "wcovby": "⩿",