diff --git a/collects/mrlib/tex-table.rkt b/collects/mrlib/tex-table.rkt index 1242bd79..88a021bf 100644 --- a/collects/mrlib/tex-table.rkt +++ b/collects/mrlib/tex-table.rkt @@ -28,15 +28,15 @@ ("leftrightarrow" "↔") ("nearrow" "↗") ("Updownarrow" "⇕") - ("hookleftarrow" "↩") - ("hookrightarrow" "↪") - ("leadsto""↝") - + ;; arrows that didn't come out right in copy & paste ;←− \longleftarrow ;⇐= \Longleftarrow + ;← 􏰂 \hookleftarrow ;←→ \longleftrightarrow + ;􏰁 → \hookrightarrow ;⇐⇒ \Longleftrightarrow + ;􏴲 \leadsto∗ ;􏰃−→ \longmapsto ;=⇒ \Longrightarrow ;􏰃→ \mapsto