Fixed TeX munge outputs of NegInf (extreal)

HOL-Theorem-Prover · Mar 19, 2024 · bbe6e63 · bbe6e63
1 parent 013d8b5
commit bbe6e63
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/real/extreal_baseScript.sml b/src/real/extreal_baseScript.sml
@@ -28,7 +28,7 @@ val _ = Unicode.unicode_version {u = UTF8.chr 0x2212 ^ UTF8.chr 0x221E,
 val _ = TeX_notation {hol = "+" ^ UTF8.chr 0x221E,
                       TeX = ("\\ensuremath{+\\infty}", 1)};
 
-val _ = TeX_notation {hol = "-" ^ UTF8.chr 0x221E,
+val _ = TeX_notation {hol = UTF8.chr 0x2212 ^ UTF8.chr 0x221E,
                       TeX = ("\\ensuremath{-\\infty}", 1)};
 
 Definition extreal_of_num_def :