--- ./doc/language/language.tex.orig	2013-02-21 08:19:16.000000000 -0700
+++ ./doc/language/language.tex	2013-02-22 11:54:34.856890763 -0700
@@ -13,6 +13,9 @@
 \usepackage{latexsym}
 %\usepackage{showidx} % shows index entries in the margin
 \usepackage[chapter]{tocbibind}
+\usepackage{amsmath}
+\usepackage{amssymb}
+\usepackage{stmaryrd}
 \usepackage{ifpdf}
 \ifpdf
 \usepackage[pdftex,dvipsnames,usenames]{color}
--- ./doc/language/pvs-doc.el.in.orig	2013-02-21 08:19:16.000000000 -0700
+++ ./doc/language/pvs-doc.el.in	2013-02-22 11:54:19.800914545 -0700
@@ -43,15 +43,128 @@
   "Return a list of which elements are characters in the STRING."
   (mapcar #'identity string))
 
+(defun unicode-to-latex (cp)
+  (case cp
+    (955 "$\\lambda$")
+    (8226 "$\\bullet$")
+    (8592 "$\\leftarrow$")
+    (8593 "$\\uparrow$")
+    (8594 "$\\rightarrow$")
+    (8595 "$\\downarrow$")
+    (8605 "$\\rightsquigarrow$")
+    (8614 "$\\mapsto$")
+    (8656 "$\\Leftarrow$")
+    (8657 "$\\Uparrow$")
+    (8658 "$\\Rightarrow$")
+    (8659 "$\\Downarrow$")
+    (8660 "$\\Leftrightarrow$")
+    (8704 "$\\forall$")
+    (8707 "$\\exists$")
+    (8711 "$\\nabla$")
+    (8712 "$\\in$")
+    (8713 "$\\notin$")
+    (8715 "$\\ni$")
+    (8723 "$\\mp$")
+    (8724 "$\\dotplus$")
+    (8728 "$\\circ$")
+    (8730 "$\\sqrt{}$")
+    (8739 "$\\mid$")
+    (8741 "$\\parallel$")
+    (8743 "$\\wedge$")
+    (8744 "$\\vee$")
+    (8745 "$\\cap$")
+    (8746 "$\\cup$")
+    (8769 "$\\nsim$")
+    (8771 "$\\eqsim$")
+    (8773 "$\\cong$")
+    (8775 "$\\ncong$")
+    (8776 "$\\approx$")
+    (8777 "$\\not\\approx$")
+    (8781 "$\\asymp$")
+    (8782 "$\\Bumpeq$")
+    (8783 "$\\bumpeq$")
+    (8784 "$\\doteq$")
+    (8791 "$\\circeq$")
+    (8793 "$\\triangleq$")
+    (8800 "$\\neq$")
+    (8801 "$\\equiv$")
+    (8804 "$\\leq$")
+    (8805 "$\\geq$")
+    (8806 "$\\leqq$")
+    (8807 "$\\geqq$")
+    (8808 "$\\lneqq$")
+    (8809 "$\\gneqq$")
+    (8810 "$\\ll$")
+    (8811 "$\\gg$")
+    (8814 "$\\nless$")
+    (8815 "$\\ngtr$")
+    (8816 "$\\nleq$")
+    (8817 "$\\ngeq$")
+    (8826 "$\\prec$")
+    (8827 "$\\succ$")
+    (8834 "$\\subset$")
+    (8835 "$\\supset$")
+    (8836 "$\\not\\subset$")
+    (8837 "$\\not\\supset$")
+    (8838 "$\\subseteq$")
+    (8839 "$\\supseteq$")
+    (8846 "$\\uplus$")
+    (8847 "$\\sqsubset$")
+    (8848 "$\\sqsupset$")
+    (8851 "$\\sqcap$")
+    (8852 "$\\sqcup$")
+    (8853 "$\\oplus$")
+    (8854 "$\\ominus$")
+    (8855 "$\\otimes$")
+    (8856 "$\\oslash$")
+    (8857 "$\\odot$")
+    (8859 "$\\circledast$")
+    (8862 "$\\boxplus$")
+    (8863 "$\\boxminus$")
+    (8864 "$\\boxtimes$")
+    (8866 "$\\boxdot$")
+    (8867 "$\\dashv$")
+    (8869 "$\\bot$")
+    (8872 "$\\vDash$")
+    (8873 "$\\vdash$")
+    (8896 "$\\bigwedge$")
+    (8897 "$\\bigvee$")
+    (8898 "$\\bigcap$")
+    (8899 "$\\bigcup$")
+    (8904 "$\\bowtie$")
+    (8968 "$\\lceil$")
+    (8969 "$\\rceil$")
+    (8970 "$\\lfloor$")
+    (8971 "$\\rfloor$")
+    (8988 "$\\ulcorner$")
+    (8989 "$\\urcorner$")
+    (8990 "$\\llcorner$")
+    (8991 "$\\lrcorner$")
+    (9001 "$\\langle$")
+    (9002 "$\\rangle$")
+    (9633 "$\\square$")
+    (9655 "$\\rhd$")
+    (9665 "$\\lhd$")
+    (9671 "$\\Diamond$")
+    (9711 "$\\bigcirc$")
+    (9733 "$\\bigstar$")
+    (10016 "$\\maltese$")
+    (10752 "$\\bigodot$")
+    (10753 "$\\bigoplus$")
+    (10754 "$\\bigotimes$")
+    (12298 "$\\ll$")
+    (12299 "$\\gg$")
+    (12314 "$\\llbracket$")
+    (12315 "$\\rrbracket$")
+    (t (concat "\\char" (format "%d" cp)))))
+
 (defun escape-tex-operator-chars (string)
   (let ((pos (- (length string) 1))
 	(chars nil))
     (while (>= pos 0)
       (setq chars
-	    (nconc
-	     (string-to-char-list (concat "\\char"
-	                                  (format "%d" (aref string pos))))
-	     chars))
+	    (nconc (string-to-char-list (unicode-to-latex (aref string pos)))
+		   chars))
       (decf pos))
     (concat chars)))