1.1 --- a/src/Tools/8bit/config/conv-tables.inp Wed Nov 05 15:47:27 1997 +0100
1.2 +++ b/src/Tools/8bit/config/conv-tables.inp Wed Nov 05 15:48:24 1997 +0100
1.3 @@ -1,14 +1,7 @@
1.4 -############################################################
1.5 -# conv-tables.inp
1.6 -# Franz Regensburger <regensbu@informatik.tu-muenchen.de>
1.7 -# 4.3.95
1.8 -#
1.9 -# last edited
1.10 -# 11.3.95
1.11 -# 20-Mar-96 by David von Oheimb: SEQ_TABLE extended
1.12 -# 10-May-96 by David von Oheimb: HI_TABLE and SEQ_TABLE rearranged
1.13 -#
1.14 -#
1.15 +# Title: Tools/8bit/config/conf-tables.inp
1.16 +# ID: $Id$
1.17 +# Author: Franz Regensburger and David von Oheimb
1.18 +# Copyright 1995 TU Muenchen
1.19 ############################################################
1.20 #
1.21 # This is the configuration file for the converter isa2latex
1.22 @@ -28,13 +21,13 @@
1.23 ############################################################
1.24 # General setup
1.25 #
1.26 -### Absolut path to the sources of the converter,
1.27 +### path to the sources of the converter,
1.28 # Must be readable for user.
1.29 #
1.30 # Must be delimited by "
1.31 #
1.32
1.33 -CONV_SOURCE_DIR "/usr/proj/isabelle/8bit/c-sources/isa2latex"
1.34 +CONV_SOURCE_DIR "../c-sources/isa2latex"
1.35
1.36 # End of general setup
1.37 ############################################################
1.38 @@ -93,17 +86,17 @@
1.39 #> "\\x22{}" double quotes are not removed
1.40 > "\x22{}" double quotes are not removed
1.41 #
1.42 -> "\#"
1.43 +> "\mbox{$\#$}"
1.44 > "\$"
1.45 > "\%"
1.46 -> "\mbox{$\&$}"
1.47 +> "\&"
1.48 > "'"
1.49 -> "("
1.50 -> ")"
1.51 -> "\mbox{$*$}"
1.52 -> "\mbox{$+$}"
1.53 +> "\mbox{$($}"
1.54 +> "\mbox{$)$}"
1.55 +> "{*}"
1.56 +> "+"
1.57 > ","
1.58 -> "\mbox{$-$}"
1.59 +> "-"
1.60 > "."
1.61 > "/"
1.62 > "0"
1.63 @@ -150,10 +143,10 @@
1.64 > "Y"
1.65 > "Z"
1.66 > "\mbox{$[$}"
1.67 -> "\mbox{$\backslash$}" Backslash
1.68 +> "\ttbackslash{}"
1.69 > "\mbox{$]$}"
1.70 > "\^{}"
1.71 -> "\_"
1.72 +> "{\_\hspace{.344ex}}"
1.73 > "`"
1.74 > "a"
1.75 > "b"
1.76 @@ -181,10 +174,10 @@
1.77 > "x"
1.78 > "y"
1.79 > "z"
1.80 -> "\{"
1.81 -> "\mbox{$|$}"
1.82 -> "\}"
1.83 -> "\~{}" negation
1.84 +> "\mbox{$\{$}" #"\ttlbrace{}"
1.85 +> "\mbox{$\mid$}"
1.86 +> "\mbox{$\}$}" #"\ttrbrace{}"
1.87 +> "\tttilde{}"
1.88 END_LOW_TABLE
1.89
1.90 ############################################################
1.91 @@ -202,7 +195,7 @@
1.92 # Must be delimited by "
1.93 #
1.94
1.95 -START_HI_TABLE "161"
1.96 +START_HI_TABLE "160"
1.97
1.98 ### The translation table HI_TABLE
1.99 #
1.100 @@ -239,120 +232,124 @@
1.101
1.102 BEGIN_HI_TABLE
1.103
1.104 +# big (i.e. double) blank space, for compensation of other too long symbols
1.105 +> "\ \ " " " "\ \ "
1.106 +
1.107 # big greek letters
1.108 -> "\\Gamma\ " "\Gamma" "\mbox{$\Gamma$}"
1.109 -> "\\Delta\ " "\Delta" "\mbox{$\Delta$}"
1.110 -> "\\Theta\ " "\Theta" "\mbox{$\Theta$}"
1.111 -> "LAM\ " "LAM" "\mbox{$\Lambda$}"
1.112 -> "\\Pi\ " "\Pi" "\mbox{$\Pi$}"
1.113 -> "\\Sigma\ " "\Sigma" "\mbox{$\Sigma$}"
1.114 -> "\\Phi\ " "\Phi" "\mbox{$\Phi$}"
1.115 -> "\\Psi\ " "\Psi" "\mbox{$\Psi$}"
1.116 -> "\\Omega\ " "\Omega" "\mbox{$\Omega$}"
1.117 +> "\\Gamma" "\Gamma" "\mbox{$\Gamma$}"
1.118 +> "\\Delta" "\Delta" "\mbox{$\Delta$}"
1.119 +> "\\Theta" "\Theta" "\mbox{$\Theta$}"
1.120 +> "LAM\ " "LAM " "\mbox{$\Lambda$}"
1.121 +> "\\Pi" "\Pi" "\mbox{$\Pi$}"
1.122 +> "\\Sigma" "\Sigma" "\mbox{$\Sigma$}"
1.123 +> "\\Phi" "\Phi" "\mbox{$\Phi$}"
1.124 +> "\\Psi" "\Psi" "\mbox{$\Psi$}"
1.125 +> "\\Omega" "\Omega" "\mbox{$\Omega$}"
1.126
1.127 # small greek letters, HOL, HOLCF
1.128 > "'a" "'a" "\mbox{$\alpha$}"
1.129 > "'b" "'b" "\mbox{$\beta$}"
1.130 > "'c" "'c" "\mbox{$\gamma$}"
1.131 -> "\\delta\ " "\delta" "\mbox{$\delta$}"
1.132 -> "\\varepsilon\ " "\varepsilon" "\mbox{$\varepsilon$}"
1.133 -> "\\zeta\ " "\zeta" "\mbox{$\zeta$}"
1.134 -> "\\eta\ " "\eta" "\mbox{$\eta$}"
1.135 -> "\\vartheta\ " "\vartheta" "\mbox{$\vartheta$}"
1.136 -> "\\kappa\ " "\kappa" "\mbox{$\kappa$}"
1.137 +> "\\delta" "\delta" "\mbox{$\delta$}"
1.138 +> "\\varepsilon" "@" "\mbox{$\varepsilon$}"
1.139 +> "\\zeta" "\zeta" "\mbox{$\zeta$}"
1.140 +> "\\eta" "\eta" "\mbox{$\eta$}"
1.141 +> "\\vartheta" "\vartheta" "\mbox{$\vartheta$}"
1.142 +> "\\kappa" "\kappa" "\mbox{$\kappa$}"
1.143 > "%\ " "%" "\mbox{$\lambda$}"
1.144 -> "\\mu\ " "\mu" "\mbox{$\mu$}"
1.145 -> "\\nu\ " "\nu" "\mbox{$\nu$}"
1.146 -> "\\xi\ " "\xi" "\mbox{$\xi$}"
1.147 -> "\\pi\ " "\pi" "\mbox{$\pi$}"
1.148 +> "\\mu" "\mu" "\mbox{$\mu$}"
1.149 +> "\\nu" "\nu" "\mbox{$\nu$}"
1.150 +> "\\xi" "\xi" "\mbox{$\xi$}"
1.151 +> "\\pi" "\p" "\mbox{$\pi$}"
1.152 > "'r" "'r" "\mbox{$\rho$}"
1.153 > "'s" "'s" "\mbox{$\sigma$}"
1.154 > "'t" "'t" "\mbox{$\tau$}"
1.155 -> "\\varphi\ " "\varphi" "\mbox{$\varphi$}"
1.156 -> "\\chi\ " "\chi" "\mbox{$\chi$}"
1.157 -> "\\psi\ " "\psi" "\mbox{$\psi$}"
1.158 -> "\\omega\ " "\omega" "\mbox{$\omega$}"
1.159 +> "\\varphi" "\varphi" "\mbox{$\varphi$}"
1.160 +> "\\chi" "\chi" "\mbox{$\chi$}"
1.161 +> "\\psi" "\psi" "\mbox{$\psi$}"
1.162 +> "\\omega" "\omega" "\mbox{$\omega$}"
1.163
1.164 # logical symbols, HOL
1.165 -> "~\ " "~" "\mbox{$\neg$}"
1.166 -> "&\ " "&" "\mbox{$\wedge$}"
1.167 -> "\|\ " "|" "\mbox{$\vee$}"
1.168 -> "!\ " "!" "\mbox{$\forall$}"
1.169 -> "\?\ " "?" "\mbox{$\exists$}"
1.170 +> "~\ " "~ " "\mbox{$\neg$}"
1.171 +> "&\ " "& " "\mbox{$\hspace{-.185ex}\wedge\hspace{-.185ex}$}\ "
1.172 +> "\|\ " "| " "\mbox{$\hspace{-.185ex}\vee\hspace{-.185ex}$}\ "
1.173 +> "!\ " "!" "\mbox{$\hspace{-.07ex}\forall$}"
1.174 +> "\?\ " "? " "\mbox{$\hspace{-.07ex}\exists$}"
1.175 > "!!" "!!" "\mbox{$\bigwedge$}"
1.176
1.177 -# parenthesis. Pure, HOLCF
1.178 -> "\\lceil\ " "\lceil" "\mbox{$\lceil$}"
1.179 -> "\\rceil\ " "\rceil" "\mbox{$\rceil$}"
1.180 -> "\\lfloor\ " "\lfloor" "\mbox{$\lfloor$}"
1.181 -> "\\rfloor\ " "\rfloor" "\mbox{$\rfloor$}"
1.182 -> "\(\|" "(|" "\mbox{$(\!|$}" #\llparenthesis
1.183 -> "\|\)" "|)" "\mbox{$|\!)$}" #\rrparenthesis
1.184 -> "\[\|" "[|" "\mbox{$[\![$}" #\llbracket
1.185 -> "\|\]" "|]" "\mbox{$]\!]$}" #\rrbracket
1.186 +# parenthesis. Pure, HOLCF, ...
1.187 +> "\\lceil" "\lceil" "\mbox{$\lceil$}"
1.188 +> "\\rceil" "\rceil" "\mbox{$\rceil$}"
1.189 +> "\\lfloor" "\lfloor" "\mbox{$\lfloor$}"
1.190 +> "\\rfloor" "\rfloor" "\mbox{$\rfloor$}"
1.191 +#> "\|-" "|-" "\mbox{$\vdash\hspace{-.2ex}$}"
1.192 +> "\|-" "|-" "\mbox{$\hspace{.49ex}\vdash\hspace{.49ex}$}"
1.193 +> "\|=" "|=" "\mbox{$\models$}"
1.194 +> "\[\|" "[|" "\mbox{$[\![\hspace{.32ex}$}"#\llbracket
1.195 +> "\|\]" "|]" "\mbox{$\hspace{.32ex}]\!]$}"#\rrbracket
1.196 +> "\\cdot" "\cdot" "\mbox{$\hspace{.28ex}\cdot\hspace{.28ex}$}"
1.197
1.198 # set theory, HOL
1.199 -> "{}" "\emptyset" "\mbox{$\emptyset$}"
1.200 -> "\ :\ " ":" "\mbox{$\in$}"
1.201 -> "\subseteq\ " "\subseteq" "\mbox{$\subseteq$}"
1.202 -> "\ Int\ " "Int" "\mbox{$\cap$}"
1.203 -> "\ Un\ " "Un" "\mbox{$\cup$}"
1.204 -> "Inter\ " "Inter" "\mbox{$\bigcap$}"
1.205 -> "Union\ " "Union" "\mbox{$\bigcup$}"
1.206 +> "\ :\ " ":" "\hspace{.1ex}\mbox{$\in$}\hspace{.1ex}"#"\mbox{$\in$}"
1.207 +> "\ \subseteq\ " " \subseteq " "\mbox{$\subseteq$}"
1.208 +> "\ Int\ " " Int " "\mbox{$\cap$}"
1.209 +> "\ Un\ " " Un " "\mbox{$\cup$}"
1.210 +> "Inter\ " "Inter " "\mbox{$\bigcap$}"
1.211 +> "Union\ " "Union " "\mbox{$\bigcup$}"
1.212
1.213 # domain theory, HOLCF
1.214 -> "\sqcap\ " "\sqcap" "\mbox{$\sqcap$}"
1.215 -> "\sqcup\ " "\sqcup" "\mbox{$\sqcup$}"
1.216 -> "glb\ " "glb" "\mbox{$\overline{|\,\,|}$}" #\bigsqcap
1.217 -> "lub\ " "lub" "\mbox{$\bigsqcup$}"
1.218 -> "UU" "UU" "\mbox{$\perp$}"
1.219 +> "\\sqcap" "\sqcap" "\mbox{$\hspace{.29ex}\sqcap\hspace{.29ex}$}"
1.220 +> "\\sqcup" "\sqcup" "\mbox{$\hspace{.29ex}\sqcup\hspace{.29ex}$}"
1.221 +> "glb\ " "glb " "\mbox{$\overline{|\,\,|}$}"#\bigsqcap
1.222 +> "LUB\ " "LUB " "\mbox{$\bigsqcup$}"
1.223 +> "UU" "UU" "\mbox{$\bot$}"
1.224
1.225 # relational symbols, Pure, HOLCF
1.226 -> "===" "===" "\mbox{$\doteq$}"
1.227 -> "==" "==" "\mbox{$\equiv$}"
1.228 +> "===" ".=" "\mbox{$\doteq$}"
1.229 +> "==" "==" "\mbox{$\hspace{.29ex}\equiv\hspace{.29ex}$}"
1.230 > "~=" "~=" "\mbox{$\not=$}"
1.231 -> "\\sqsubset\ " "\sqsubset" "\mbox{$\sqsubset$}"
1.232 -> "<<" "<<" "\mbox{$\sqsubseteq$}"
1.233 -> "\\prec\ " "\prec" "\mbox{$\prec$}"
1.234 -> "\\preceq\ " "\preceq" "\mbox{$\preceq$}"
1.235 -> "\\succ\ " "\succ" "\mbox{$\succ$}"
1.236 -> "\\succeq\ " "\succeq" "\mbox{$\succeq$}"
1.237 -> "\\sim\ " "\sim" "\mbox{$\sim$}"
1.238 -> "\\simeq\ " "\simeq" "\mbox{$\simeq$}"
1.239 -> "\\le\ " "\le" "\mbox{$\le$}"
1.240 -> "\\ge\ " "\ge" "\mbox{$\ge$}"
1.241 +> "\\sqsubset" "\sqsubset" "\mbox{$\hspace{.29ex}\sqsubset\hspace{.29ex}$}"
1.242 +> "<<" "<<" "\mbox{$\hspace{.29ex}\sqsubseteq\hspace{.29ex}$}"
1.243 +> "<:" "<:" "\mbox{$\hspace{.29ex}\prec\hspace{.29ex}$}\ "
1.244 +> "<=:" "<=:" "\mbox{$\hspace{.29ex}\preceq\hspace{.29ex}$}"
1.245 +> ":>" ":>" "\mbox{$\hspace{.29ex}\succ\hspace{.29ex}$}\ "
1.246 +> "~~" "~~" "\mbox{$\hspace{.29ex}\approx\hspace{.29ex}$}"
1.247 +> "\\sim\ " "\sim " "\mbox{$\hspace{.29ex}\sim\hspace{.29ex}$}\ "
1.248 +> "\\simeq" "\simeq" "\mbox{$\hspace{.29ex}\simeq\hspace{.29ex}$}"
1.249 +> "<=" "<=" "\mbox{$\hspace{.29ex}\le\hspace{.29ex}$}"
1.250 +> "::" "::" "\mbox{$\hspace{-.1ex}:\hspace{-.07ex}:\hspace{.1ex}$}"
1.251
1.252 # arrows, Pure, HOL
1.253 > "<-" "<-" "\mbox{$\leftarrow$}"
1.254 > "-@@@@@" "-" "\mbox{$-$}"
1.255 > "->" "->" "\mbox{$\rightarrow$}"
1.256 -> "\\Leftarrow\ " "<=" "\mbox{$\Leftarrow$}"
1.257 +> "\\Leftarrow" "<=" "\mbox{$\Leftarrow$}"
1.258 > "=@@@@@" "=" "\mbox{$=$}"
1.259 -> "=>" "=>" "\mbox{$\Rightarrow$}"
1.260 -> "->>" "->>" "\mbox{$\twoheadrightarrow$}"
1.261 -> "\\mapsto\ " "\mapsto" "\mbox{$\mapsto$}"
1.262 -> "\\leadsto\ " "\leadsto" "\mbox{$\leadsto$}"
1.263 -> "\\uparrow\ " "\uparrow" "\mbox{$\uparrow$}"
1.264 -> "\\downarrow\ " "\downarrow" "\mbox{$\downarrow$}"
1.265 +> "=>" "=>" "\mbox{$\hspace{.12ex}\Rightarrow$}"
1.266 +> "\\frown" "\frown" "\mbox{$\frown$}"
1.267 +> "\\mapsto" "|->" "\mbox{$\mapsto$}"
1.268 +> "\\leadsto" "~>" "\mbox{$\hspace{.05ex}\leadsto$}"
1.269 +> "\\uparrow" "\uparrow" "\mbox{$\uparrow$}"
1.270 +> "\\downarrow" "\downarrow" "\mbox{$\downarrow$}"
1.271 > "~:" "~:" "\mbox{$\notin$}"
1.272
1.273 # arithmetic, HOLCF
1.274 -> "\\times\ " "*" "\mbox{$\times$}"
1.275 -> "\\oplus\ " "++" "\mbox{$\oplus$}" #\varoplus
1.276 -> "\\ominus\ " "\ominus" "\mbox{$\ominus$}" " #\varominus
1.277 -> "\\otimes\ " "**" "\mbox{$\otimes$}" " #\varotimes
1.278 -> "\\oslash\ " "\oslash" "\mbox{$\oslash$}" #\varoslash
1.279 -> "\\natural\ " "\natural" "\mbox{$\natural$}"
1.280 -> "\\infty\ " "\infty" "\mbox{$\infty$}"
1.281 +> "\\times" "*" "\mbox{$\hspace{-.29ex}\times\hspace{-.29ex}$}"
1.282 +> "\\oplus" "++" "\mbox{$\hspace{.29ex}\oplus\hspace{.29ex}$}" #\varoplus
1.283 +> "\\ominus" "--" "\mbox{$\hspace{.29ex}\ominus\hspace{.29ex}$}" #\varominus
1.284 +> "\\otimes" "**" "\mbox{$\hspace{.29ex}\otimes\hspace{.29ex}$}" #\varotimes
1.285 +> "\\oslash" "//" "\mbox{$\hspace{.29ex}\oslash\hspace{.29ex}$}" #\varoslash
1.286 +> "\\subset" "\subset" "\mbox{$\subset$}"
1.287 +> "\\infty" "\infty" "\mbox{$\infty$}"
1.288
1.289 # misc
1.290 -> "\\Box\ " "\Box" "\mbox{$\Box$}"
1.291 -> "\\Diamond\ " "\Diamond" "\mbox{$\Diamond$}"
1.292 -> "\\circ\ " "\circ" "\mbox{$\circ$}"
1.293 -> "\\bullet\ " "\bullet" "\mbox{$\bullet$}"
1.294 +> "\\Box" "\Box" "\mbox{$\Box$}"
1.295 +> "\\Diamond" "<>" "\mbox{$\hspace{.29ex}\Diamond\hspace{.29ex}$}"
1.296 +> "\\circ" " o " "\mbox{$\circ$}"
1.297 +> "\\bullet" "\bullet" "\mbox{$\bullet$}"
1.298 > "\|\|" "||" "\mbox{$\parallel$}"
1.299 -> "\\tick\ " "\tick" "\mbox{$\surd$}"
1.300 -> "\\filter\ " "\filter" "\mbox{\copyright}"
1.301 +> "\\tick" "\tick" "\mbox{$\surd$}"
1.302 +> "\\filter" "\filter" "\mbox{\copyright}"
1.303 END_HI_TABLE
1.304
1.305 ############################################################
1.306 @@ -392,21 +389,41 @@
1.307 BEGIN_SEQ_TABLE
1.308
1.309 # Pure
1.310 -> "êë" "==>" "==>" "\mbox{$\Longrightarrow$}"
1.311 +> "êë" "==>" "==>" "\mbox{$\hspace{-.083ex}\Longrightarrow$}"
1.312
1.313 # HOL
1.314 > "çè" "-->" "-->" "\mbox{$\longrightarrow$}"
1.315 -> "Ã!" "\?!" "?!" "\mbox{$\exists$}!"
1.316 -> "ALL@@@@@" "ALL\ " "ALL" "\mbox{$\forall$}"
1.317 -> "EX@@@@@" "EX\ " "EX" "\mbox{$\exists$}"
1.318 +> "Ã!" "\?!" "?!" "\mbox{$\exists_1$}"
1.319 +> "ALL@@@@@" "ALL\ " "ALL " "\mbox{$\forall$}"
1.320 +> "EX@@@@@" "EX\ " "EX " "\mbox{$\exists$}"
1.321
1.322 #HOLCF
1.323 -> "<\|@@@@@" "<\|" "<|" "\mbox{$<\!\mid$}"
1.324 -> "<<\|@@@@@" "<<\|" "<<|" "\mbox{$\ll\!\mid$}"
1.325 +> "<<\|" "<<\|" "<<|" "\mbox{$\ll\!\mid$}"
1.326 +> "<\|" "<\|" "<|" "\mbox{$<\!\mid$}"
1.327
1.328 # misc ?
1.329 > "éê" "<==" "<==" "\mbox{$\Longleftarrow$}"
1.330 > "éë" "<=>" "<=>" "\mbox{$\Leftrightarrow$}"
1.331 > "æç" "<--" "<--" "\mbox{$\longleftarrow$}"
1.332 -> "æè" "<->" "<->" "\mbox{$\leftrightarrow$}"
1.333 +> "æè" "<->" "<->""\mbox{$\leftrightarrow$}"
1.334 +> "\^-1" "\^-1" "^-1" "\mbox{$^{\tt -1}$}"
1.335 +
1.336 +#Isabelle
1.337 +> "arities" "@arities" "arities" "\mbox{\bf arities}"
1.338 +> "axclass" "@axclass" "axclass" "\mbox{\bf axclass}"
1.339 +> "constdefs" "@constdefs" "constdefs" "\mbox{\bf constdefs}"
1.340 +> "consts" "@consts" "consts" "\mbox{\bf consts}"
1.341 +> "datatype" "@datatype" "datatype" "\mbox{\bf datatype}"
1.342 +> "defs" "@defs" "defs" "\mbox{\bf defs}"
1.343 +> "domain" "@domain" "domain" "\mbox{\bf domain}"
1.344 +> "inductive" "@inductive" "inductive" "\mbox{\bf inductive}"
1.345 +> "instance" "@instance" "instance" "\mbox{\bf instance}"
1.346 +> "primrec" "@primrec" "primrec" "\mbox{\bf primrec}"
1.347 +> "recdef" "@recdef" "recdef" "\mbox{\bf recdef}"
1.348 +> "rules" "@rules" "rules" "\mbox{\bf rules}"
1.349 +> "translations""@translations""translations" "\mbox{\bf translations}"
1.350 +> "typedef" "@typedef" "typedef" "\mbox{\bf typedef}"
1.351 +> "types" "@types" "types" "\mbox{\bf types}"
1.352 END_SEQ_TABLE
1.353 +
1.354 +