%format <+	  = " \ensuremath{ \mathbin{\triangleleft} } "
%format <*	  = "\mathbin{\ooalign{\hfil\hspace{1pt}\hbox{$\cdot$}\hfil\crcr$\triangleleft$}}"
%format ...	  = "\ensuremath{\mathbin{\textrm{..}}}"
%format ....	  = "\ensuremath{\mathbin{\textrm{...}}}"
%format .-.	  = "\ensuremath{\mathbin{\textrm{-\hskip0.1ex-}}}"
%format .--.	  = "\ensuremath{\mathbin{\textrm{-\hskip0.1ex-\hskip0.1ex-}}}"
%format .&.	  = "\ensuremath{\mathbin{\textrm{\&}}}"
%format .=	  = "\ensuremath{\mathrel{\doteq}}"
%format .<	  = "\ensuremath{\mathbin{\dot{<}}}"
%format .<=	  = "\ensuremath{\mathbin{\dot{\leq}}}"
%format .==	  = "\ensuremath{\mathbin{\dot{\equiv}}}"
%format ./=	  = "\ensuremath{\mathbin{\dot{\not\equiv}}}"
%format .*	  = "\ensuremath{\mathbin{\dot{*}}}"
%format |-|	  = "\ensuremath{\mathbin{\POver }}"
%format |=|	  = "\ensuremath{\phantom{}\mathbin{\PSOver}}"
%format |||	  = "\ensuremath{\mathbin{\PBeside}}"
%format ||||	  = "\ensuremath{\phantom{}\mathbin{\PSBeside}}"
%format par1	  = "\ensuremath{\textit{par}_1}"
%format parn	  = "\ensuremath{\textit{par}_n}"
%format a0	  = "\ensuremath{a_0}"
%format a1	  = "\ensuremath{a_1}"
%format a2	  = "\ensuremath{a_2}"
%format a3	  = "\ensuremath{a_3}"
%format b0	  = "\ensuremath{b_0}"
%format b1	  = "\ensuremath{b_1}"
%format b2	  = "\ensuremath{b_2}"
%format b3	  = "\ensuremath{b_3}"
%format c0	  = "\ensuremath{c_0}"
%format c1	  = "\ensuremath{c_1}"
%format c2	  = "\ensuremath{c_2}"
%format c3	  = "\ensuremath{c_3}"
%format d0	  = "\ensuremath{d_0}"
%format d1	  = "\ensuremath{d_1}"
%format d2	  = "\ensuremath{d_2}"
%format d3	  = "\ensuremath{d_3}"
%format e0	  = "\ensuremath{e_0}"
%format e1	  = "\ensuremath{e_1}"
%format e2	  = "\ensuremath{e_2}"
%format e3	  = "\ensuremath{e_3}"
%format f0	  = "\ensuremath{f_0}"
%format f1	  = "\ensuremath{f_1}"
%format f2	  = "\ensuremath{f_2}"
%format f3	  = "\ensuremath{f_3}"
%format g0	  = "\ensuremath{g_0}"
%format g1	  = "\ensuremath{g_1}"
%format g2	  = "\ensuremath{g_2}"
%format g3	  = "\ensuremath{g_3}"
%format h0	  = "\ensuremath{h_0}"
%format h1	  = "\ensuremath{h_1}"
%format h2	  = "\ensuremath{h_2}"
%format h3	  = "\ensuremath{h_3}"
%format i0	  = "\ensuremath{i_0}"
%format i1	  = "\ensuremath{i_1}"
%format i2	  = "\ensuremath{i_2}"
%format i3	  = "\ensuremath{i_3}"
%format j0	  = "\ensuremath{j_0}"
%format j1	  = "\ensuremath{j_1}"
%format j2	  = "\ensuremath{j_2}"
%format j3	  = "\ensuremath{j_3}"
%format k0	  = "\ensuremath{k_0}"
%format k1	  = "\ensuremath{k_1}"
%format k2	  = "\ensuremath{k_2}"
%format k3	  = "\ensuremath{k_3}"
%format l0	  = "\ensuremath{l_0}"
%format l1	  = "\ensuremath{l_1}"
%format l2	  = "\ensuremath{l_2}"
%format l3	  = "\ensuremath{l_3}"
%format m0	  = "\ensuremath{m_0}"
%format m1	  = "\ensuremath{m_1}"
%format m2	  = "\ensuremath{m_2}"
%format m3	  = "\ensuremath{m_3}"
%format n0	  = "\ensuremath{n_0}"
%format n1	  = "\ensuremath{n_1}"
%format n2	  = "\ensuremath{n_2}"
%format n3	  = "\ensuremath{n_3}"
%format o0	  = "\ensuremath{o_0}"
%format o1	  = "\ensuremath{o_1}"
%format o2	  = "\ensuremath{o_2}"
%format o3	  = "\ensuremath{o_3}"
%format p0	  = "\ensuremath{p_0}"
%format p1	  = "\ensuremath{p_1}"
%format p2	  = "\ensuremath{p_2}"
%format p3	  = "\ensuremath{p_3}"
%format p4	  = "\ensuremath{p_4}"
%format p5	  = "\ensuremath{p_5}"
%format p6	  = "\ensuremath{p_6}"
%format p_n	  = "\ensuremath{p_n}"
%format q0	  = "\ensuremath{q_0}"
%format q1	  = "\ensuremath{q_1}"
%format q2	  = "\ensuremath{q_2}"
%format q3	  = "\ensuremath{q_3}"
%format r0	  = "\ensuremath{r_0}"
%format r1	  = "\ensuremath{r_1}"
%format r2	  = "\ensuremath{r_2}"
%format r3	  = "\ensuremath{r_3}"
%format s0	  = "\ensuremath{s_0}"
%format s1	  = "\ensuremath{s_1}"
%format s2	  = "\ensuremath{s_2}"
%format s3	  = "\ensuremath{s_3}"
%format t0	  = "\ensuremath{t_0}"
%format t1	  = "\ensuremath{t_1}"
%format t2	  = "\ensuremath{t_2}"
%format t3	  = "\ensuremath{t_3}"
%format t4	  = "\ensuremath{t_4}"
%format u0	  = "\ensuremath{u_0}"
%format u1	  = "\ensuremath{u_1}"
%format u2	  = "\ensuremath{u_2}"
%format u3	  = "\ensuremath{u_3}"
%format v0	  = "\ensuremath{v_0}"
%format v1	  = "\ensuremath{v_1}"
%format v2	  = "\ensuremath{v_2}"
%format v3	  = "\ensuremath{v_3}"
%format w0	  = "\ensuremath{w_0}"
%format w1	  = "\ensuremath{w_1}"
%format w2	  = "\ensuremath{w_2}"
%format w3	  = "\ensuremath{w_3}"
%format x0	  = "\ensuremath{x_0}"
%format x1	  = "\ensuremath{x_1}"
%format x2	  = "\ensuremath{x_2}"
%format x3	  = "\ensuremath{x_3}"
%format y0	  = "\ensuremath{y_0}"
%format y1	  = "\ensuremath{y_1}"
%format y2	  = "\ensuremath{y_2}"
%format y3	  = "\ensuremath{y_3}"
%format z0	  = "\ensuremath{z_0}"
%format z1	  = "\ensuremath{z_1}"
%format z2	  = "\ensuremath{z_2}"
%format z3	  = "\ensuremath{z_3}"
%format z4	  = "\ensuremath{z_4}"
%format z5	  = "\ensuremath{z_5}"
%format z6	  = "\ensuremath{z_6}"
%format z7	  = "\ensuremath{z_7}"
%format z8	  = "\ensuremath{z_8}"
%format z9	  = "\ensuremath{z_9}"
%format div13	  = "\ensuremath{\frac{1}{3}}"
%format div12	  = "\ensuremath{\frac{1}{2}}"
%format #	  = "\ensuremath{\phantom{}\mathbin{\mbox{\#}}}"
%format &	  = "\ensuremath{\mathbin{\textrm{\&}}}"
%format cycle'	  = " cycle "
%format default'  = " default "

%format <+>	  = "\mathbin{\ooalign{\hfil\raise1.5pt\hbox{$\scriptscriptstyle +$}\hfil\crcr\hbox{$<>$}}}"
%format $+$	  = "\mathbin{\ooalign{\hbox{$\$\mskip-4mu\$ $}}}"
%format $$	  = "\mathbin{\ooalign{\hbox{$\$\mskip-4mu\$ $}}}"

%format >+>	  = "\hspace{0.8em}"
%format \=	  = "}$\=${"
%format \=/	  = "\="
%format \=$	  = "$\=$\phantom{}"
%format \>	  = "}$\>${"
%format \>/	  = "\>"
%format \>$	  = "$\>$\phantom{}"

%format setred	  = "\color{red}\mskip-\thickmuskip"
%format setblack  = "\color{black}\mskip-\thickmuskip"

%format &<	  = "\ensuremath{\langle}"
%format &>	  = "\ensuremath{\rangle}"


%subst verb a		= "\text{\tt " a "}"
%subst verbatim a	= "\begin{tabbing}\tt'n" a "'n\end{tabbing}'n"
%subst verbnl		= "\\'n\tt "
%format \\	= "$\setminus$"
%if style == tt
%subst inline a  = "\text{\texfamily " a "}"
%subst thinspace = "\Sp "
%subst code a    = "\begin{tabbing}\texfamily'n" a "'n\end{tabbing}'n"
%subst comment a = "{\rmfamily-{}- " a "}"
%subst nested a  = "{\rmfamily\enskip\{- " a " -\}\enskip}"
%subst spaces a  = a
%subst special a = a
%subst space     = "~"
%subst newline   = "\\'n\texfamily "
%subst conid a   = "{\itshape " a "}"
%subst varid a   = a
%subst consym a  = a
%subst varsym a  = a
%subst numeral a = a
%subst char a    = a
%subst string a  = a
%if underlineKeywords
%subst keyword a = "\uline{" a "}"
%else
%subst keyword a = "{\bfseries " a "}"
%endif
%format \         = "\char''10"
%format .         = "\char''00"
%if not spacePreserving
%format alpha     = "\char''02"
%format beta      = "\char''03"
%format gamma     = "\char''11"
%format delta     = "\char''12"
%format pi        = "\char''07"
%format infty     = "\char''16"
%format intersect = "\char''22"
%format union     = "\char''23"
%format forall    = "\char''24"
%format exists    = "\char''25"
%format not       = "\char''05"
%format &&        = "\char''04"
%format ||        = "\char''37"
%format <-        = "\char''06"
%format ->        = "\char''31"
%format ==        = "\char''36"
%format /=        = "\char''32"
%format <=        = "\char''34"
%format >=        = "\char''35"
%endif
%if meta
%format M.a = "\ensuremath{a}"
%format M.b = "\ensuremath{b}"
%format M.alpha   = "\ensuremath{\alpha}"
%format M.beta    = "\ensuremath{\beta}"
%format M.forall  = "\ensuremath{\forall}"
%format M.exists  = "\ensuremath{\exists}"
%format M.not     = "\ensuremath{\neg}"
%format ==>       = "\ensuremath{\Longrightarrow}"
%format <==       = "\ensuremath{\Longleftarrow}"
%format /\        = "\ensuremath{\wedge}"
%format \/        = "\ensuremath{\vee}"
%format M.=       = "\ensuremath{=}"
%format M./=      = "\ensuremath{\neq}"
%format M.<       = "\ensuremath{<}"
%format M.<=      = "\ensuremath{\leq}"
%format M.>=      = "\ensuremath{\geq}"
%format M.>       = "\ensuremath{>}"
%endif
%elif style == math
%let autoSpacing	= True
%subst dummy		= "\cdot "
%subst inline a  	= "\ensuremath{" a "}"
%subst comment a	= "\mbox{\qquad-{}- " a "}"
%subst nested a	= "\mbox{\enskip\{- " a " -\}\enskip}"
%subst hskip a	= "\hskip" a "em\relax"
%subst phantom a	= "\phantom{" a "\mbox{}}"
%if array
%subst code a    	= "\[\begin{array}{@{}lcl}'n\hspace{\lwidht}&\hspace{\cwidth}&\\[-10pt]'n" a "'n\end{array}\]"
%subst column3 l c r	= "{}" l " & " c " & {" r "}"
%subst column1 a	= "\multicolumn{3}{@{}l}{" a "}"
%else
%subst code a    	= "\begin{tabbing}'n\qquad\=\hspace{\lwidht}\=\hspace{\cwidth}\=\+\kill'n" a "'n\end{tabbing}"
%subst column3 l c r	= "$" l "$ \> \makebox[\cwidth]{$" c "$} \> ${" r "}$"
%subst column1 a	= "$" a "$"
%endif
%subst spaces a		= a
%subst special a	= a
%subst space     	= "\;"
%subst newline   	= "\\'n"
%subst blankline 	= "\\[1mm]'n"
%subst conid a   	= "\Conid{" a "}"
%subst varid a   	= "\Varid{" a "}"
%subst consym a  	= "\mathbin{" a "}"
%subst varsym a  	= "\mathbin{" a "}"
%subst numeral a 	= "\mathrm{" a "}"
%subst char a    	= "\text{\tt " a "}"
%subst string a  	= "\text{\tt " a "}"
%subst keyword a 	= "\mathbf{" a "}"
%format _          = "\anonymous "
%format ->         = "\to "
%format <-         = "\leftarrow "
%format =>         = "\ensuremath{\Rightarrow }"
%format \          = "\lambda "
%format |          = "|\mskip1.5mu "
%format {          = "\{\mskip1.5mu "
%format }          = "\mskip1.5mu\}"
%format [          = "[\mskip1.5mu "
%format ]          = "\mskip1.5mu]"
%format =          = "\mathrel{=}"
%format ..         = "\mathinner{\ldotp\ldotp}"
%format ~          =  "\mathord{\sim}"
%format @          =  "\mathord{@}"
%format .          = "\mathbin{\circ}"
%format !!         = "\mathbin{!!}"
%format ^          = "\mathbin{\uparrow}"
%format ^^         = "\mathbin{\uparrow\uparrow}"
%format **         = "\mathbin{**}"
%format /          = "\mathbin{/}"
%format `quot`     = "\mathbin{\Varid{`quot`}}"
%format `rem`      = "\mathbin{\Varid{`rem`}}"
%format `div`      = "\mathbin{\Varid{`div`}}"
%format `mod`      = "\mathbin{\Varid{`mod`}}"
%format :%         = "\mathbin{:\%}"
%format %          = "\mathbin{\%}"
%format :          = "\mathbin{:}"
%format ++         = "\plus "
%format ==         = "\equiv "
%% ODER: format ==         = "\mathrel{==}"
%format /=         = "\not\equiv "
%% ODER: format /=         = "\neq "
%format <=         = "\leq "
%format >=         = "\geq "
%format `elem`     = "\in "
%format `notElem`  = "\notin "
%format &&         = "\mathrel{\wedge}"
%%format &          = "\&"
%format ||         = "\mathrel{\vee}"
%format >>         = "\sequ "
%format >>=        = "\bind "
%format $          = "\mathbin{\$}"
%format `seq`      = "\mathbin{\Varid{`seq`}}"
%%format !          = "\mathbin{!}"
%format //         = "\mathbin{//}"
%format undefined  = "\bot "
%format not	   = "\neg "
%if meta
%format M.a = "a"
%format M.b = "b"
%format M.alpha   = "\alpha "
%format M.beta    = "\beta "
%format M.forall  = "\forall "
%format M.exists  = "\exists "
%format M.not     = "\neg "
%format ==>       = "\enskip\Longrightarrow\enskip "
%format <==       = "\enskip\Longleftarrow\enskip "
%format /\        = "\enskip\mathrel{\wedge}\enskip "
%format \/        = "\enskip\mathrel{\vee}\enskip "
%format M.=       = "="
%format M./=      = "\neq "
%format M.<       = "<"
%format M.<=      = "\leq "
%format M.>=      = "\geq "
%format M.>       = ">"
%endif
%endif