diff -r 93448766eb5a -r 26ebb89cc1d7 src/Tools/8bit/config/conv-tables.inp --- a/src/Tools/8bit/config/conv-tables.inp Wed Nov 05 15:47:27 1997 +0100 +++ b/src/Tools/8bit/config/conv-tables.inp Wed Nov 05 15:48:24 1997 +0100 @@ -1,14 +1,7 @@ -############################################################ -# conv-tables.inp -# Franz Regensburger -# 4.3.95 -# -# last edited -# 11.3.95 -# 20-Mar-96 by David von Oheimb: SEQ_TABLE extended -# 10-May-96 by David von Oheimb: HI_TABLE and SEQ_TABLE rearranged -# -# +# Title: Tools/8bit/config/conf-tables.inp +# ID: $Id$ +# Author: Franz Regensburger and David von Oheimb +# Copyright 1995 TU Muenchen ############################################################ # # This is the configuration file for the converter isa2latex @@ -28,13 +21,13 @@ ############################################################ # General setup # -### Absolut path to the sources of the converter, +### path to the sources of the converter, # Must be readable for user. # # Must be delimited by " # -CONV_SOURCE_DIR "/usr/proj/isabelle/8bit/c-sources/isa2latex" +CONV_SOURCE_DIR "../c-sources/isa2latex" # End of general setup ############################################################ @@ -93,17 +86,17 @@ #> "\\x22{}" double quotes are not removed > "\x22{}" double quotes are not removed # -> "\#" +> "\mbox{$\#$}" > "\$" > "\%" -> "\mbox{$\&$}" +> "\&" > "'" -> "(" -> ")" -> "\mbox{$*$}" -> "\mbox{$+$}" +> "\mbox{$($}" +> "\mbox{$)$}" +> "{*}" +> "+" > "," -> "\mbox{$-$}" +> "-" > "." > "/" > "0" @@ -150,10 +143,10 @@ > "Y" > "Z" > "\mbox{$[$}" -> "\mbox{$\backslash$}" Backslash +> "\ttbackslash{}" > "\mbox{$]$}" > "\^{}" -> "\_" +> "{\_\hspace{.344ex}}" > "`" > "a" > "b" @@ -181,10 +174,10 @@ > "x" > "y" > "z" -> "\{" -> "\mbox{$|$}" -> "\}" -> "\~{}" negation +> "\mbox{$\{$}" #"\ttlbrace{}" +> "\mbox{$\mid$}" +> "\mbox{$\}$}" #"\ttrbrace{}" +> "\tttilde{}" END_LOW_TABLE ############################################################ @@ -202,7 +195,7 @@ # Must be delimited by " # -START_HI_TABLE "161" +START_HI_TABLE "160" ### The translation table HI_TABLE # @@ -239,120 +232,124 @@ BEGIN_HI_TABLE +# big (i.e. double) blank space, for compensation of other too long symbols +> "\ \ " " " "\ \ " + # big greek letters -> "\\Gamma\ " "\Gamma" "\mbox{$\Gamma$}" -> "\\Delta\ " "\Delta" "\mbox{$\Delta$}" -> "\\Theta\ " "\Theta" "\mbox{$\Theta$}" -> "LAM\ " "LAM" "\mbox{$\Lambda$}" -> "\\Pi\ " "\Pi" "\mbox{$\Pi$}" -> "\\Sigma\ " "\Sigma" "\mbox{$\Sigma$}" -> "\\Phi\ " "\Phi" "\mbox{$\Phi$}" -> "\\Psi\ " "\Psi" "\mbox{$\Psi$}" -> "\\Omega\ " "\Omega" "\mbox{$\Omega$}" +> "\\Gamma" "\Gamma" "\mbox{$\Gamma$}" +> "\\Delta" "\Delta" "\mbox{$\Delta$}" +> "\\Theta" "\Theta" "\mbox{$\Theta$}" +> "LAM\ " "LAM " "\mbox{$\Lambda$}" +> "\\Pi" "\Pi" "\mbox{$\Pi$}" +> "\\Sigma" "\Sigma" "\mbox{$\Sigma$}" +> "\\Phi" "\Phi" "\mbox{$\Phi$}" +> "\\Psi" "\Psi" "\mbox{$\Psi$}" +> "\\Omega" "\Omega" "\mbox{$\Omega$}" # small greek letters, HOL, HOLCF > "'a" "'a" "\mbox{$\alpha$}" > "'b" "'b" "\mbox{$\beta$}" > "'c" "'c" "\mbox{$\gamma$}" -> "\\delta\ " "\delta" "\mbox{$\delta$}" -> "\\varepsilon\ " "\varepsilon" "\mbox{$\varepsilon$}" -> "\\zeta\ " "\zeta" "\mbox{$\zeta$}" -> "\\eta\ " "\eta" "\mbox{$\eta$}" -> "\\vartheta\ " "\vartheta" "\mbox{$\vartheta$}" -> "\\kappa\ " "\kappa" "\mbox{$\kappa$}" +> "\\delta" "\delta" "\mbox{$\delta$}" +> "\\varepsilon" "@" "\mbox{$\varepsilon$}" +> "\\zeta" "\zeta" "\mbox{$\zeta$}" +> "\\eta" "\eta" "\mbox{$\eta$}" +> "\\vartheta" "\vartheta" "\mbox{$\vartheta$}" +> "\\kappa" "\kappa" "\mbox{$\kappa$}" > "%\ " "%" "\mbox{$\lambda$}" -> "\\mu\ " "\mu" "\mbox{$\mu$}" -> "\\nu\ " "\nu" "\mbox{$\nu$}" -> "\\xi\ " "\xi" "\mbox{$\xi$}" -> "\\pi\ " "\pi" "\mbox{$\pi$}" +> "\\mu" "\mu" "\mbox{$\mu$}" +> "\\nu" "\nu" "\mbox{$\nu$}" +> "\\xi" "\xi" "\mbox{$\xi$}" +> "\\pi" "\p" "\mbox{$\pi$}" > "'r" "'r" "\mbox{$\rho$}" > "'s" "'s" "\mbox{$\sigma$}" > "'t" "'t" "\mbox{$\tau$}" -> "\\varphi\ " "\varphi" "\mbox{$\varphi$}" -> "\\chi\ " "\chi" "\mbox{$\chi$}" -> "\\psi\ " "\psi" "\mbox{$\psi$}" -> "\\omega\ " "\omega" "\mbox{$\omega$}" +> "\\varphi" "\varphi" "\mbox{$\varphi$}" +> "\\chi" "\chi" "\mbox{$\chi$}" +> "\\psi" "\psi" "\mbox{$\psi$}" +> "\\omega" "\omega" "\mbox{$\omega$}" # logical symbols, HOL -> "~\ " "~" "\mbox{$\neg$}" -> "&\ " "&" "\mbox{$\wedge$}" -> "\|\ " "|" "\mbox{$\vee$}" -> "!\ " "!" "\mbox{$\forall$}" -> "\?\ " "?" "\mbox{$\exists$}" +> "~\ " "~ " "\mbox{$\neg$}" +> "&\ " "& " "\mbox{$\hspace{-.185ex}\wedge\hspace{-.185ex}$}\ " +> "\|\ " "| " "\mbox{$\hspace{-.185ex}\vee\hspace{-.185ex}$}\ " +> "!\ " "!" "\mbox{$\hspace{-.07ex}\forall$}" +> "\?\ " "? " "\mbox{$\hspace{-.07ex}\exists$}" > "!!" "!!" "\mbox{$\bigwedge$}" -# parenthesis. Pure, HOLCF -> "\\lceil\ " "\lceil" "\mbox{$\lceil$}" -> "\\rceil\ " "\rceil" "\mbox{$\rceil$}" -> "\\lfloor\ " "\lfloor" "\mbox{$\lfloor$}" -> "\\rfloor\ " "\rfloor" "\mbox{$\rfloor$}" -> "\(\|" "(|" "\mbox{$(\!|$}" #\llparenthesis -> "\|\)" "|)" "\mbox{$|\!)$}" #\rrparenthesis -> "\[\|" "[|" "\mbox{$[\![$}" #\llbracket -> "\|\]" "|]" "\mbox{$]\!]$}" #\rrbracket +# parenthesis. Pure, HOLCF, ... +> "\\lceil" "\lceil" "\mbox{$\lceil$}" +> "\\rceil" "\rceil" "\mbox{$\rceil$}" +> "\\lfloor" "\lfloor" "\mbox{$\lfloor$}" +> "\\rfloor" "\rfloor" "\mbox{$\rfloor$}" +#> "\|-" "|-" "\mbox{$\vdash\hspace{-.2ex}$}" +> "\|-" "|-" "\mbox{$\hspace{.49ex}\vdash\hspace{.49ex}$}" +> "\|=" "|=" "\mbox{$\models$}" +> "\[\|" "[|" "\mbox{$[\![\hspace{.32ex}$}"#\llbracket +> "\|\]" "|]" "\mbox{$\hspace{.32ex}]\!]$}"#\rrbracket +> "\\cdot" "\cdot" "\mbox{$\hspace{.28ex}\cdot\hspace{.28ex}$}" # set theory, HOL -> "{}" "\emptyset" "\mbox{$\emptyset$}" -> "\ :\ " ":" "\mbox{$\in$}" -> "\subseteq\ " "\subseteq" "\mbox{$\subseteq$}" -> "\ Int\ " "Int" "\mbox{$\cap$}" -> "\ Un\ " "Un" "\mbox{$\cup$}" -> "Inter\ " "Inter" "\mbox{$\bigcap$}" -> "Union\ " "Union" "\mbox{$\bigcup$}" +> "\ :\ " ":" "\hspace{.1ex}\mbox{$\in$}\hspace{.1ex}"#"\mbox{$\in$}" +> "\ \subseteq\ " " \subseteq " "\mbox{$\subseteq$}" +> "\ Int\ " " Int " "\mbox{$\cap$}" +> "\ Un\ " " Un " "\mbox{$\cup$}" +> "Inter\ " "Inter " "\mbox{$\bigcap$}" +> "Union\ " "Union " "\mbox{$\bigcup$}" # domain theory, HOLCF -> "\sqcap\ " "\sqcap" "\mbox{$\sqcap$}" -> "\sqcup\ " "\sqcup" "\mbox{$\sqcup$}" -> "glb\ " "glb" "\mbox{$\overline{|\,\,|}$}" #\bigsqcap -> "lub\ " "lub" "\mbox{$\bigsqcup$}" -> "UU" "UU" "\mbox{$\perp$}" +> "\\sqcap" "\sqcap" "\mbox{$\hspace{.29ex}\sqcap\hspace{.29ex}$}" +> "\\sqcup" "\sqcup" "\mbox{$\hspace{.29ex}\sqcup\hspace{.29ex}$}" +> "glb\ " "glb " "\mbox{$\overline{|\,\,|}$}"#\bigsqcap +> "LUB\ " "LUB " "\mbox{$\bigsqcup$}" +> "UU" "UU" "\mbox{$\bot$}" # relational symbols, Pure, HOLCF -> "===" "===" "\mbox{$\doteq$}" -> "==" "==" "\mbox{$\equiv$}" +> "===" ".=" "\mbox{$\doteq$}" +> "==" "==" "\mbox{$\hspace{.29ex}\equiv\hspace{.29ex}$}" > "~=" "~=" "\mbox{$\not=$}" -> "\\sqsubset\ " "\sqsubset" "\mbox{$\sqsubset$}" -> "<<" "<<" "\mbox{$\sqsubseteq$}" -> "\\prec\ " "\prec" "\mbox{$\prec$}" -> "\\preceq\ " "\preceq" "\mbox{$\preceq$}" -> "\\succ\ " "\succ" "\mbox{$\succ$}" -> "\\succeq\ " "\succeq" "\mbox{$\succeq$}" -> "\\sim\ " "\sim" "\mbox{$\sim$}" -> "\\simeq\ " "\simeq" "\mbox{$\simeq$}" -> "\\le\ " "\le" "\mbox{$\le$}" -> "\\ge\ " "\ge" "\mbox{$\ge$}" +> "\\sqsubset" "\sqsubset" "\mbox{$\hspace{.29ex}\sqsubset\hspace{.29ex}$}" +> "<<" "<<" "\mbox{$\hspace{.29ex}\sqsubseteq\hspace{.29ex}$}" +> "<:" "<:" "\mbox{$\hspace{.29ex}\prec\hspace{.29ex}$}\ " +> "<=:" "<=:" "\mbox{$\hspace{.29ex}\preceq\hspace{.29ex}$}" +> ":>" ":>" "\mbox{$\hspace{.29ex}\succ\hspace{.29ex}$}\ " +> "~~" "~~" "\mbox{$\hspace{.29ex}\approx\hspace{.29ex}$}" +> "\\sim\ " "\sim " "\mbox{$\hspace{.29ex}\sim\hspace{.29ex}$}\ " +> "\\simeq" "\simeq" "\mbox{$\hspace{.29ex}\simeq\hspace{.29ex}$}" +> "<=" "<=" "\mbox{$\hspace{.29ex}\le\hspace{.29ex}$}" +> "::" "::" "\mbox{$\hspace{-.1ex}:\hspace{-.07ex}:\hspace{.1ex}$}" # arrows, Pure, HOL > "<-" "<-" "\mbox{$\leftarrow$}" > "-@@@@@" "-" "\mbox{$-$}" > "->" "->" "\mbox{$\rightarrow$}" -> "\\Leftarrow\ " "<=" "\mbox{$\Leftarrow$}" +> "\\Leftarrow" "<=" "\mbox{$\Leftarrow$}" > "=@@@@@" "=" "\mbox{$=$}" -> "=>" "=>" "\mbox{$\Rightarrow$}" -> "->>" "->>" "\mbox{$\twoheadrightarrow$}" -> "\\mapsto\ " "\mapsto" "\mbox{$\mapsto$}" -> "\\leadsto\ " "\leadsto" "\mbox{$\leadsto$}" -> "\\uparrow\ " "\uparrow" "\mbox{$\uparrow$}" -> "\\downarrow\ " "\downarrow" "\mbox{$\downarrow$}" +> "=>" "=>" "\mbox{$\hspace{.12ex}\Rightarrow$}" +> "\\frown" "\frown" "\mbox{$\frown$}" +> "\\mapsto" "|->" "\mbox{$\mapsto$}" +> "\\leadsto" "~>" "\mbox{$\hspace{.05ex}\leadsto$}" +> "\\uparrow" "\uparrow" "\mbox{$\uparrow$}" +> "\\downarrow" "\downarrow" "\mbox{$\downarrow$}" > "~:" "~:" "\mbox{$\notin$}" # arithmetic, HOLCF -> "\\times\ " "*" "\mbox{$\times$}" -> "\\oplus\ " "++" "\mbox{$\oplus$}" #\varoplus -> "\\ominus\ " "\ominus" "\mbox{$\ominus$}" " #\varominus -> "\\otimes\ " "**" "\mbox{$\otimes$}" " #\varotimes -> "\\oslash\ " "\oslash" "\mbox{$\oslash$}" #\varoslash -> "\\natural\ " "\natural" "\mbox{$\natural$}" -> "\\infty\ " "\infty" "\mbox{$\infty$}" +> "\\times" "*" "\mbox{$\hspace{-.29ex}\times\hspace{-.29ex}$}" +> "\\oplus" "++" "\mbox{$\hspace{.29ex}\oplus\hspace{.29ex}$}" #\varoplus +> "\\ominus" "--" "\mbox{$\hspace{.29ex}\ominus\hspace{.29ex}$}" #\varominus +> "\\otimes" "**" "\mbox{$\hspace{.29ex}\otimes\hspace{.29ex}$}" #\varotimes +> "\\oslash" "//" "\mbox{$\hspace{.29ex}\oslash\hspace{.29ex}$}" #\varoslash +> "\\subset" "\subset" "\mbox{$\subset$}" +> "\\infty" "\infty" "\mbox{$\infty$}" # misc -> "\\Box\ " "\Box" "\mbox{$\Box$}" -> "\\Diamond\ " "\Diamond" "\mbox{$\Diamond$}" -> "\\circ\ " "\circ" "\mbox{$\circ$}" -> "\\bullet\ " "\bullet" "\mbox{$\bullet$}" +> "\\Box" "\Box" "\mbox{$\Box$}" +> "\\Diamond" "<>" "\mbox{$\hspace{.29ex}\Diamond\hspace{.29ex}$}" +> "\\circ" " o " "\mbox{$\circ$}" +> "\\bullet" "\bullet" "\mbox{$\bullet$}" > "\|\|" "||" "\mbox{$\parallel$}" -> "\\tick\ " "\tick" "\mbox{$\surd$}" -> "\\filter\ " "\filter" "\mbox{\copyright}" +> "\\tick" "\tick" "\mbox{$\surd$}" +> "\\filter" "\filter" "\mbox{\copyright}" END_HI_TABLE ############################################################ @@ -392,21 +389,41 @@ BEGIN_SEQ_TABLE # Pure -> "êë" "==>" "==>" "\mbox{$\Longrightarrow$}" +> "êë" "==>" "==>" "\mbox{$\hspace{-.083ex}\Longrightarrow$}" # HOL > "çè" "-->" "-->" "\mbox{$\longrightarrow$}" -> "Ã!" "\?!" "?!" "\mbox{$\exists$}!" -> "ALL@@@@@" "ALL\ " "ALL" "\mbox{$\forall$}" -> "EX@@@@@" "EX\ " "EX" "\mbox{$\exists$}" +> "Ã!" "\?!" "?!" "\mbox{$\exists_1$}" +> "ALL@@@@@" "ALL\ " "ALL " "\mbox{$\forall$}" +> "EX@@@@@" "EX\ " "EX " "\mbox{$\exists$}" #HOLCF -> "<\|@@@@@" "<\|" "<|" "\mbox{$<\!\mid$}" -> "<<\|@@@@@" "<<\|" "<<|" "\mbox{$\ll\!\mid$}" +> "<<\|" "<<\|" "<<|" "\mbox{$\ll\!\mid$}" +> "<\|" "<\|" "<|" "\mbox{$<\!\mid$}" # misc ? > "éê" "<==" "<==" "\mbox{$\Longleftarrow$}" > "éë" "<=>" "<=>" "\mbox{$\Leftrightarrow$}" > "æç" "<--" "<--" "\mbox{$\longleftarrow$}" -> "æè" "<->" "<->" "\mbox{$\leftrightarrow$}" +> "æè" "<->" "<->""\mbox{$\leftrightarrow$}" +> "\^-1" "\^-1" "^-1" "\mbox{$^{\tt -1}$}" + +#Isabelle +> "arities" "@arities" "arities" "\mbox{\bf arities}" +> "axclass" "@axclass" "axclass" "\mbox{\bf axclass}" +> "constdefs" "@constdefs" "constdefs" "\mbox{\bf constdefs}" +> "consts" "@consts" "consts" "\mbox{\bf consts}" +> "datatype" "@datatype" "datatype" "\mbox{\bf datatype}" +> "defs" "@defs" "defs" "\mbox{\bf defs}" +> "domain" "@domain" "domain" "\mbox{\bf domain}" +> "inductive" "@inductive" "inductive" "\mbox{\bf inductive}" +> "instance" "@instance" "instance" "\mbox{\bf instance}" +> "primrec" "@primrec" "primrec" "\mbox{\bf primrec}" +> "recdef" "@recdef" "recdef" "\mbox{\bf recdef}" +> "rules" "@rules" "rules" "\mbox{\bf rules}" +> "translations""@translations""translations" "\mbox{\bf translations}" +> "typedef" "@typedef" "typedef" "\mbox{\bf typedef}" +> "types" "@types" "types" "\mbox{\bf types}" END_SEQ_TABLE + +