# HG changeset patch
# User oheimb
# Date 905267001 -7200
# Node ID cff7d1e9837635fac8b5010688966e63f71e4c3d
# Parent  2487121d3bd10100f1243e7cdf9b7d33227db3d7
improved spacing

diff -r 2487121d3bd1 -r cff7d1e98376 src/Tools/8bit/c-sources/isa2latex/conv-lex.x
--- a/src/Tools/8bit/c-sources/isa2latex/conv-lex.x	Tue Sep 08 16:06:04 1998 +0200
+++ b/src/Tools/8bit/c-sources/isa2latex/conv-lex.x	Tue Sep 08 17:03:21 1998 +0200
@@ -183,9 +183,9 @@
 <ISAA>\\downarrow     	put((char)240,FALSE,0);
 <ISAA>~:              	put((char)241,FALSE,0);
 <ISAA>\\times         	put((char)242,FALSE,0);
-<ISAA>\\oplus         	put((char)243,FALSE,0);
+<ISAA>\+\+            	put((char)243,FALSE,0);
 <ISAA>\\ominus        	put((char)244,FALSE,0);
-<ISAA>\\otimes        	put((char)245,FALSE,0);
+<ISAA>\*\*            	put((char)245,FALSE,0);
 <ISAA>\\oslash        	put((char)246,FALSE,0);
 <ISAA>\\subset        	put((char)247,FALSE,0);
 <ISAA>\\infty         	put((char)248,FALSE,0);
diff -r 2487121d3bd1 -r cff7d1e98376 src/Tools/8bit/c-sources/isa2latex/conv-tables.h
--- a/src/Tools/8bit/c-sources/isa2latex/conv-tables.h	Tue Sep 08 16:06:04 1998 +0200
+++ b/src/Tools/8bit/c-sources/isa2latex/conv-tables.h	Tue Sep 08 17:03:21 1998 +0200
@@ -154,7 +154,7 @@
    {"\\chi"       ,"\\mbox{$\\chi$}"},
    {"\\psi"       ,"\\mbox{$\\psi$}"},
    {"\\omega"     ,"\\mbox{$\\omega$}"},
-   {"~ "          ,"\\mbox{$\\neg$}"},
+   {"~ "          ,"\\mbox{$\\hspace{-.33ex}\\neg$}"},
    {"& "          ,"\\mbox{$\\hspace{-.185ex}\\wedge\\hspace{-.185ex}$}\\ "},
    {"| "          ,"\\mbox{$\\hspace{-.185ex}\\vee\\hspace{-.185ex}$}\\ "},
    {"!"           ,"\\mbox{$\\hspace{-.07ex}\\forall$}"},
@@ -169,7 +169,7 @@
    {"[|"          ,"\\mbox{$[\\![\\hspace{.32ex}$}"},
    {"|]"          ,"\\mbox{$\\hspace{.32ex}]\\!]$}"},
    {"."           ,"\\mbox{$\\hspace{.28ex}\\cdot\\hspace{.28ex}$}"},
-   {":"           ,"\\hspace{.1ex}\\mbox{$\\in$}\\hspace{.1ex}"},
+   {":"           ,"\\mbox{$\\hspace{.445ex}\\in\\hspace{.445ex}$}"},
    {" <= "        ,"\\mbox{$\\subseteq$}"},
    {" Int "       ,"\\mbox{$\\cap$}"},
    {" Un "        ,"\\mbox{$\\cup$}"},
@@ -179,10 +179,10 @@
    {"\\sqcup"     ,"\\mbox{$\\hspace{.29ex}\\sqcup\\hspace{.29ex}$}"},
    {"glb "        ,"\\mbox{$\\overline{|\\,\\,|}$}"},
    {"LUB "        ,"\\mbox{$\\bigsqcup$}"},
-   {"UU"          ,"\\mbox{$\\bot$}"},
+   {"UU"          ,"\\mbox{$\\hspace{-.29ex}\\bot\\hspace{-.29ex}$}"},
    {".="          ,"\\mbox{$\\doteq$}"},
    {"=="          ,"\\mbox{$\\hspace{.29ex}\\equiv\\hspace{.29ex}$}"},
-   {"~="          ,"\\mbox{$\\not=$}"},
+   {"~="          ,"\\mbox{$\\hspace{-.34ex}\\not\\hspace{-.3ex}\\mbox{=}$}"},
    {"\\sqsubset"  ,"\\mbox{$\\hspace{.29ex}\\sqsubset\\hspace{.29ex}$}"},
    {"<<"          ,"\\mbox{$\\hspace{.29ex}\\sqsubseteq\\hspace{.29ex}$}"},
    {"<:"          ,"\\mbox{$\\hspace{.29ex}\\prec\\hspace{.29ex}$}\\ "},
@@ -204,7 +204,7 @@
    {"~>"          ,"\\mbox{$\\hspace{.05ex}\\leadsto$}"},
    {"\\uparrow"   ,"\\mbox{$\\uparrow$}"},
    {"\\downarrow" ,"\\mbox{$\\downarrow$}"},
-   {"~:"          ,"\\mbox{$\\notin$}"},
+   {"~:"          ,"\\mbox{$\\hspace{.445ex}\\notin\\hspace{.445ex}$}"},
    {"*"           ,"\\mbox{$\\hspace{-.29ex}\\times\\hspace{-.29ex}$}"},
    {"++"          ,"\\mbox{$\\hspace{.29ex}\\oplus\\hspace{.29ex}$}"},
    {"--"          ,"\\mbox{$\\hspace{.29ex}\\ominus\\hspace{.29ex}$}"},
diff -r 2487121d3bd1 -r cff7d1e98376 src/Tools/8bit/config/conv-tables.inp
--- a/src/Tools/8bit/config/conv-tables.inp	Tue Sep 08 16:06:04 1998 +0200
+++ b/src/Tools/8bit/config/conv-tables.inp	Tue Sep 08 17:03:21 1998 +0200
@@ -270,7 +270,7 @@
 >  "\\omega"		"\omega"	"\mbox{$\omega$}" 
 
 # logical symbols, HOL
->  "~\ "		"~ "		"\mbox{$\neg$}" 
+>  "~\ "		"~ "		"\mbox{$\hspace{-.33ex}\neg$}" 
 >  "&\ "		"& "		"\mbox{$\hspace{-.185ex}\wedge\hspace{-.185ex}$}\ " 
 >  "\|\ "		"| "		"\mbox{$\hspace{-.185ex}\vee\hspace{-.185ex}$}\ " 
 >  "!\ "		"!"		"\mbox{$\hspace{-.07ex}\forall$}" 
@@ -290,7 +290,7 @@
 >  "\\cdot"		"."		"\mbox{$\hspace{.28ex}\cdot\hspace{.28ex}$}"
 
 # set theory, HOL
->  "\ :\ "		":"		"\hspace{.1ex}\mbox{$\in$}\hspace{.1ex}"#"\mbox{$\in$}"
+>  "\ :\ "		":"		"\mbox{$\hspace{.445ex}\in\hspace{.445ex}$}"
 >  "\ \subseteq\ "	" <= "		"\mbox{$\subseteq$}" 
 >  "\ Int\ "		" Int "		"\mbox{$\cap$}" 
 >  "\ Un\ "		" Un "		"\mbox{$\cup$}" 
@@ -302,12 +302,12 @@
 >  "\\sqcup"		"\sqcup"	"\mbox{$\hspace{.29ex}\sqcup\hspace{.29ex}$}" 
 >  "glb\ "		"glb "		"\mbox{$\overline{|\,\,|}$}"#\bigsqcap
 >  "LUB\ "		"LUB "		"\mbox{$\bigsqcup$}" 
->  "UU"			"UU"		"\mbox{$\bot$}" 
+>  "UU"			"UU"		"\mbox{$\hspace{-.29ex}\bot\hspace{-.29ex}$}" 
 
 # relational symbols, Pure, HOLCF
 >  "==="		".="		"\mbox{$\doteq$}" 
 >  "=="			"=="		"\mbox{$\hspace{.29ex}\equiv\hspace{.29ex}$}" 
->  "~="			"~="		"\mbox{$\not=$}" 
+>  "~="			"~="		"\mbox{$\hspace{-.34ex}\not\hspace{-.3ex}\mbox{=}$}" 
 >  "\\sqsubset"		"\sqsubset"	"\mbox{$\hspace{.29ex}\sqsubset\hspace{.29ex}$}" 
 >  "<<"			"<<"		"\mbox{$\hspace{.29ex}\sqsubseteq\hspace{.29ex}$}" 
 >  "<:"			"<:"		"\mbox{$\hspace{.29ex}\prec\hspace{.29ex}$}\ " 
@@ -331,13 +331,13 @@
 >  "\\leadsto"		"~>"		"\mbox{$\hspace{.05ex}\leadsto$}" 
 >  "\\uparrow"		"\uparrow"	"\mbox{$\uparrow$}" 
 >  "\\downarrow"	"\downarrow"	"\mbox{$\downarrow$}" 
->  "~:"			"~:"		"\mbox{$\notin$}" 
+>  "~:"			"~:"		"\mbox{$\hspace{.445ex}\notin\hspace{.445ex}$}" 
 
 # arithmetic, HOLCF
 >  "\\times"		"*"		"\mbox{$\hspace{-.29ex}\times\hspace{-.29ex}$}" 
->  "\\oplus"		"++"		"\mbox{$\hspace{.29ex}\oplus\hspace{.29ex}$}"	#\varoplus
+>  "\+\+"		"++"		"\mbox{$\hspace{.29ex}\oplus\hspace{.29ex}$}"	#\varoplus
 >  "\\ominus"		"--"		"\mbox{$\hspace{.29ex}\ominus\hspace{.29ex}$}"	#\varominus
->  "\\otimes"		"**"		"\mbox{$\hspace{.29ex}\otimes\hspace{.29ex}$}"	#\varotimes
+>  "\*\*"		"**"		"\mbox{$\hspace{.29ex}\otimes\hspace{.29ex}$}"	#\varotimes
 >  "\\oslash"		"//"		"\mbox{$\hspace{.29ex}\oslash\hspace{.29ex}$}" 	#\varoslash
 >  "\\subset"		"\subset"	"\mbox{$\subset$}" 
 >  "\\infty"		"\infty"	"\mbox{$\infty$}"