| "\\upharpoonleft" -> (tex_use_ams (); LITERAL (TEX_ONLY "\\upharpoonleft "))
| "\\downharpoonright" -> (tex_use_ams (); LITERAL (TEX_ONLY "\\downharpoonright "))
| "\\downharpoonleft" -> (tex_use_ams (); LITERAL (TEX_ONLY "\\downharpoonleft "))
+ | "\\rightharpoonup" -> (tex_use_ams (); LITERAL (TEX_ONLY "\\rightharpoonup "))
+ | "\\rightharpoondown" -> (tex_use_ams (); LITERAL (TEX_ONLY "\\rightharpoondown "))
+ | "\\leftharpoonup" -> (tex_use_ams (); LITERAL (TEX_ONLY "\\leftharpoonup "))
+ | "\\leftharpoondown" -> (tex_use_ams (); LITERAL (TEX_ONLY "\\leftharpoondown "))
| "\\nless" -> (tex_use_ams (); LITERAL (TEX_ONLY "\\nless "))
| "\\Vdash" -> (tex_use_ams (); LITERAL (TEX_ONLY "\\Vdash "))
| "\\vDash" -> (tex_use_ams (); LITERAL (TEX_ONLY "\\vDash "))