various improvements
authoroheimb
Wed Nov 05 15:48:24 1997 +0100 (1997-11-05)
changeset 417226ebb89cc1d7
parent 4171 93448766eb5a
child 4173 e87fa74113aa
various improvements
src/Tools/8bit/config/conv-tables.inp
     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 +