--- 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);
--- 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}$}"},
--- 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$}"