author | oheimb |
Fri, 24 Apr 1998 16:15:34 +0200 | |
changeset 4826 | 44d38b2737e2 |
parent 4773 | b6729feb8a5d |
child 5436 | cff7d1e98376 |
permissions | -rw-r--r-- |
4172 | 1 |
# Title: Tools/8bit/config/conf-tables.inp |
2 |
# ID: $Id$ |
|
3 |
# Author: Franz Regensburger and David von Oheimb |
|
4 |
# Copyright 1995 TU Muenchen |
|
1826 | 5 |
############################################################ |
6 |
# |
|
7 |
# This is the configuration file for the converter isa2latex |
|
8 |
# It is interpreted by the perl script `gen-isa2latex' which |
|
9 |
# produces rsp. changes the followong files of the converter |
|
10 |
# sources: |
|
11 |
# |
|
12 |
# Makefile, conv-tables.h, conv-defs.h and conv-lex.x |
|
13 |
# |
|
14 |
# In the perl script, regular expressions are used to identify |
|
15 |
# the keywords. In order to be sure that something is treated |
|
16 |
# as a comment, simply begin the line with a # sign. This is |
|
17 |
# fool proof. |
|
18 |
# |
|
19 |
############################################################ |
|
20 |
||
21 |
############################################################ |
|
22 |
# General setup |
|
23 |
# |
|
4172 | 24 |
### path to the sources of the converter, |
1826 | 25 |
# Must be readable for user. |
26 |
# |
|
27 |
# Must be delimited by " |
|
28 |
# |
|
29 |
||
4639 | 30 |
CONV_SOURCE_DIR "../c-sources/isa2latex" |
1826 | 31 |
|
32 |
# End of general setup |
|
33 |
############################################################ |
|
34 |
||
35 |
############################################################ |
|
36 |
# Setup for translationTableLow in file conv-tables.h |
|
37 |
# |
|
38 |
||
39 |
### Start index START_LOW_TABLE of translationTableLow |
|
40 |
# The index END_LOW_TABLE is computed from the length |
|
41 |
# of the translation table LOW_TABLE below. |
|
42 |
# |
|
43 |
# constraints: 32 <= START_LOW_TABLE <= 127 |
|
44 |
# START_LOW_TABLE + length(LOW_TABLE) - 1 <= 127 |
|
45 |
# |
|
46 |
# Must be delimited by " |
|
47 |
# |
|
48 |
||
49 |
START_LOW_TABLE "32" |
|
50 |
||
51 |
### The translation table LOW_TABLE |
|
52 |
# |
|
53 |
# Keyword for the begin of the table is BEGIN_LOW_TABLE |
|
54 |
# Keyword for the end of the table is END_LOW_TABLE |
|
55 |
# |
|
56 |
# Lines beginning with # are ignored as everywhere in this file. |
|
57 |
# Lines obeying the syntax given below are treated as table entries. |
|
58 |
# All other lines are ignored, too. This is for comments. |
|
59 |
# |
|
60 |
# Syntax of a table entry: |
|
61 |
# |
|
62 |
# > "LaTeX replacement" anything |
|
63 |
# |
|
64 |
# The double quotes enclose the LaTeX replacement in pure |
|
65 |
# LaTeX syntax. |
|
66 |
# Every \ in the string except when used for hex-notation \x?? is |
|
67 |
# automatically duplicated by the script! The strings are used in |
|
68 |
# printf output statements in the C code. |
|
69 |
# |
|
70 |
# Attention: you have to use hex-notation \x22 to produce a " inside |
|
71 |
# the double quoted strings. An explicit " will terminate the string. |
|
72 |
# |
|
73 |
# The following `anything' is ignored by the perl script. |
|
74 |
# This is for comments. |
|
75 |
# |
|
76 |
# The ordering of entries in the table LOW_TABLE is relevant! |
|
77 |
# Empty table is not allowed. |
|
78 |
# |
|
79 |
# |
|
80 |
||
81 |
BEGIN_LOW_TABLE |
|
82 |
> "\ " Blank |
|
83 |
> "!" |
|
84 |
# |
|
85 |
# if you don't like double quotes to be removed insert the following |
|
86 |
#> "\\x22{}" double quotes are not removed |
|
87 |
> "\x22{}" double quotes are not removed |
|
88 |
# |
|
4773
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4639
diff
changeset
|
89 |
> "\#" |
1826 | 90 |
> "\$" |
91 |
> "\%" |
|
4172 | 92 |
> "\&" |
1826 | 93 |
> "'" |
4773
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4639
diff
changeset
|
94 |
> "(" |
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4639
diff
changeset
|
95 |
> ")" |
4172 | 96 |
> "{*}" |
97 |
> "+" |
|
1826 | 98 |
> "," |
4172 | 99 |
> "-" |
1826 | 100 |
> "." |
101 |
> "/" |
|
102 |
> "0" |
|
103 |
> "1" |
|
104 |
> "2" |
|
105 |
> "3" |
|
106 |
> "4" |
|
107 |
> "5" |
|
108 |
> "6" |
|
109 |
> "7" |
|
110 |
> "8" |
|
111 |
> "9" |
|
112 |
> ":" |
|
113 |
> ";" |
|
4773
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4639
diff
changeset
|
114 |
> "<" |
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4639
diff
changeset
|
115 |
> "=" |
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4639
diff
changeset
|
116 |
> ">" |
1826 | 117 |
> "?" |
118 |
> "@" |
|
119 |
> "A" |
|
120 |
> "B" |
|
121 |
> "C" |
|
122 |
> "D" |
|
123 |
> "E" |
|
124 |
> "F" |
|
125 |
> "G" |
|
126 |
> "H" |
|
127 |
> "I" |
|
128 |
> "J" |
|
129 |
> "K" |
|
130 |
> "L" |
|
131 |
> "M" |
|
132 |
> "N" |
|
133 |
> "O" |
|
134 |
> "P" |
|
135 |
> "Q" |
|
136 |
> "R" |
|
137 |
> "S" |
|
138 |
> "T" |
|
139 |
> "U" |
|
140 |
> "V" |
|
141 |
> "W" |
|
142 |
> "X" |
|
143 |
> "Y" |
|
144 |
> "Z" |
|
4773
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4639
diff
changeset
|
145 |
> "[" |
4639 | 146 |
> "\ttbackslash{}" #????? |
4773
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4639
diff
changeset
|
147 |
> "]" |
1826 | 148 |
> "\^{}" |
4172 | 149 |
> "{\_\hspace{.344ex}}" |
1826 | 150 |
> "`" |
151 |
> "a" |
|
152 |
> "b" |
|
153 |
> "c" |
|
154 |
> "d" |
|
155 |
> "e" |
|
156 |
> "f" |
|
157 |
> "g" |
|
158 |
> "h" |
|
159 |
> "i" |
|
160 |
> "j" |
|
161 |
> "k" |
|
162 |
> "l" |
|
163 |
> "m" |
|
164 |
> "n" |
|
165 |
> "o" |
|
166 |
> "p" |
|
167 |
> "q" |
|
168 |
> "r" |
|
169 |
> "s" |
|
170 |
> "t" |
|
171 |
> "u" |
|
172 |
> "v" |
|
173 |
> "w" |
|
174 |
> "x" |
|
175 |
> "y" |
|
176 |
> "z" |
|
4773
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4639
diff
changeset
|
177 |
> "\{" #"\ttlbrace{}" |
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4639
diff
changeset
|
178 |
> "|" |
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4639
diff
changeset
|
179 |
> "\}" #"\ttrbrace{}" |
4172 | 180 |
> "\tttilde{}" |
1826 | 181 |
END_LOW_TABLE |
182 |
||
183 |
############################################################ |
|
184 |
# Setup for translationTableHi in file conv-tables.h |
|
185 |
# |
|
186 |
||
187 |
### Start index START_HI_TABLE of translationTableHi |
|
188 |
# The index END_HI_TABLE is computed from the length |
|
189 |
# of the translation table HI_TABLE below. |
|
190 |
# |
|
191 |
# constraints: 128 <= START_HI_TABLE <= 255 |
|
192 |
# START_HI_TABLE + length(HI_TABLE) - 1 <= 255 |
|
193 |
# |
|
194 |
# |
|
195 |
# Must be delimited by " |
|
196 |
# |
|
197 |
||
4172 | 198 |
START_HI_TABLE "160" |
1826 | 199 |
|
200 |
### The translation table HI_TABLE |
|
201 |
# |
|
202 |
# Keyword for the begin of the table is BEGIN_HI_TABLE |
|
203 |
# Keyword for the end of the table is END_HI_TABLE |
|
204 |
# |
|
205 |
# Lines beginning with # are ignored as everywhere in this file. |
|
206 |
# Lines obeying the syntax given below are treated as table entries. |
|
207 |
# All other lines are ignored, too. This is for comments. |
|
208 |
# |
|
209 |
# Syntax of a table entry: |
|
210 |
# |
|
211 |
# > "lex expression ascii" "ascii replacement" "LaTeX replacement" anything |
|
212 |
# |
|
213 |
# The double quotes enclose the lex expression, the ascii replacement, and the |
|
214 |
# LaTeX replacement in pure lex rsp. pure ascii rsp. LaTeX syntax. |
|
215 |
# |
|
216 |
# The string for the lex expression is literally passed to lex. Backslashes |
|
217 |
# are not duplicated! |
|
218 |
# Every \ in the replacements except when used for hex-notation \x?? is |
|
219 |
# automatically duplicated by the script! The strings are used in |
|
220 |
# printf output statements in the C code. |
|
221 |
# |
|
222 |
# Attention: you have to use hex-notation \x22 to produce a " inside |
|
223 |
# the double quoted strings. An explicit " will terminate the string. |
|
224 |
# |
|
225 |
# The following `anything' is ignored by the perl script. |
|
226 |
# This is for comments. |
|
227 |
# |
|
228 |
# The ordering of entries in the table HI_TABLE is relevant! |
|
229 |
# Empty table is not allowed. |
|
230 |
# |
|
231 |
# |
|
232 |
||
233 |
BEGIN_HI_TABLE |
|
234 |
||
4172 | 235 |
# big (i.e. double) blank space, for compensation of other too long symbols |
236 |
> "\ \ " " " "\ \ " |
|
237 |
||
1826 | 238 |
# big greek letters |
4172 | 239 |
> "\\Gamma" "\Gamma" "\mbox{$\Gamma$}" |
240 |
> "\\Delta" "\Delta" "\mbox{$\Delta$}" |
|
241 |
> "\\Theta" "\Theta" "\mbox{$\Theta$}" |
|
242 |
> "LAM\ " "LAM " "\mbox{$\Lambda$}" |
|
243 |
> "\\Pi" "\Pi" "\mbox{$\Pi$}" |
|
244 |
> "\\Sigma" "\Sigma" "\mbox{$\Sigma$}" |
|
245 |
> "\\Phi" "\Phi" "\mbox{$\Phi$}" |
|
246 |
> "\\Psi" "\Psi" "\mbox{$\Psi$}" |
|
247 |
> "\\Omega" "\Omega" "\mbox{$\Omega$}" |
|
1826 | 248 |
|
249 |
# small greek letters, HOL, HOLCF |
|
250 |
> "'a" "'a" "\mbox{$\alpha$}" |
|
251 |
> "'b" "'b" "\mbox{$\beta$}" |
|
252 |
> "'c" "'c" "\mbox{$\gamma$}" |
|
4172 | 253 |
> "\\delta" "\delta" "\mbox{$\delta$}" |
254 |
> "\\varepsilon" "@" "\mbox{$\varepsilon$}" |
|
255 |
> "\\zeta" "\zeta" "\mbox{$\zeta$}" |
|
256 |
> "\\eta" "\eta" "\mbox{$\eta$}" |
|
257 |
> "\\vartheta" "\vartheta" "\mbox{$\vartheta$}" |
|
258 |
> "\\kappa" "\kappa" "\mbox{$\kappa$}" |
|
1826 | 259 |
> "%\ " "%" "\mbox{$\lambda$}" |
4172 | 260 |
> "\\mu" "\mu" "\mbox{$\mu$}" |
261 |
> "\\nu" "\nu" "\mbox{$\nu$}" |
|
262 |
> "\\xi" "\xi" "\mbox{$\xi$}" |
|
263 |
> "\\pi" "\p" "\mbox{$\pi$}" |
|
1826 | 264 |
> "'r" "'r" "\mbox{$\rho$}" |
265 |
> "'s" "'s" "\mbox{$\sigma$}" |
|
266 |
> "'t" "'t" "\mbox{$\tau$}" |
|
4172 | 267 |
> "\\varphi" "\varphi" "\mbox{$\varphi$}" |
268 |
> "\\chi" "\chi" "\mbox{$\chi$}" |
|
269 |
> "\\psi" "\psi" "\mbox{$\psi$}" |
|
270 |
> "\\omega" "\omega" "\mbox{$\omega$}" |
|
1826 | 271 |
|
272 |
# logical symbols, HOL |
|
4172 | 273 |
> "~\ " "~ " "\mbox{$\neg$}" |
274 |
> "&\ " "& " "\mbox{$\hspace{-.185ex}\wedge\hspace{-.185ex}$}\ " |
|
275 |
> "\|\ " "| " "\mbox{$\hspace{-.185ex}\vee\hspace{-.185ex}$}\ " |
|
276 |
> "!\ " "!" "\mbox{$\hspace{-.07ex}\forall$}" |
|
277 |
> "\?\ " "? " "\mbox{$\hspace{-.07ex}\exists$}" |
|
1826 | 278 |
> "!!" "!!" "\mbox{$\bigwedge$}" |
279 |
||
4172 | 280 |
# parenthesis. Pure, HOLCF, ... |
281 |
> "\\lceil" "\lceil" "\mbox{$\lceil$}" |
|
282 |
> "\\rceil" "\rceil" "\mbox{$\rceil$}" |
|
283 |
> "\\lfloor" "\lfloor" "\mbox{$\lfloor$}" |
|
284 |
> "\\rfloor" "\rfloor" "\mbox{$\rfloor$}" |
|
285 |
#> "\|-" "|-" "\mbox{$\vdash\hspace{-.2ex}$}" |
|
286 |
> "\|-" "|-" "\mbox{$\hspace{.49ex}\vdash\hspace{.49ex}$}" |
|
287 |
> "\|=" "|=" "\mbox{$\models$}" |
|
288 |
> "\[\|" "[|" "\mbox{$[\![\hspace{.32ex}$}"#\llbracket |
|
289 |
> "\|\]" "|]" "\mbox{$\hspace{.32ex}]\!]$}"#\rrbracket |
|
4639 | 290 |
> "\\cdot" "." "\mbox{$\hspace{.28ex}\cdot\hspace{.28ex}$}" |
1826 | 291 |
|
292 |
# set theory, HOL |
|
4172 | 293 |
> "\ :\ " ":" "\hspace{.1ex}\mbox{$\in$}\hspace{.1ex}"#"\mbox{$\in$}" |
4826 | 294 |
> "\ \subseteq\ " " <= " "\mbox{$\subseteq$}" |
4172 | 295 |
> "\ Int\ " " Int " "\mbox{$\cap$}" |
296 |
> "\ Un\ " " Un " "\mbox{$\cup$}" |
|
4639 | 297 |
> "Inter\ " "INT " "\mbox{$\bigcap$}" |
298 |
> "Union\ " "UN " "\mbox{$\bigcup$}" |
|
1826 | 299 |
|
300 |
# domain theory, HOLCF |
|
4172 | 301 |
> "\\sqcap" "\sqcap" "\mbox{$\hspace{.29ex}\sqcap\hspace{.29ex}$}" |
302 |
> "\\sqcup" "\sqcup" "\mbox{$\hspace{.29ex}\sqcup\hspace{.29ex}$}" |
|
303 |
> "glb\ " "glb " "\mbox{$\overline{|\,\,|}$}"#\bigsqcap |
|
304 |
> "LUB\ " "LUB " "\mbox{$\bigsqcup$}" |
|
305 |
> "UU" "UU" "\mbox{$\bot$}" |
|
1826 | 306 |
|
307 |
# relational symbols, Pure, HOLCF |
|
4172 | 308 |
> "===" ".=" "\mbox{$\doteq$}" |
309 |
> "==" "==" "\mbox{$\hspace{.29ex}\equiv\hspace{.29ex}$}" |
|
1826 | 310 |
> "~=" "~=" "\mbox{$\not=$}" |
4172 | 311 |
> "\\sqsubset" "\sqsubset" "\mbox{$\hspace{.29ex}\sqsubset\hspace{.29ex}$}" |
312 |
> "<<" "<<" "\mbox{$\hspace{.29ex}\sqsubseteq\hspace{.29ex}$}" |
|
313 |
> "<:" "<:" "\mbox{$\hspace{.29ex}\prec\hspace{.29ex}$}\ " |
|
314 |
> "<=:" "<=:" "\mbox{$\hspace{.29ex}\preceq\hspace{.29ex}$}" |
|
315 |
> ":>" ":>" "\mbox{$\hspace{.29ex}\succ\hspace{.29ex}$}\ " |
|
316 |
> "~~" "~~" "\mbox{$\hspace{.29ex}\approx\hspace{.29ex}$}" |
|
317 |
> "\\sim\ " "\sim " "\mbox{$\hspace{.29ex}\sim\hspace{.29ex}$}\ " |
|
318 |
> "\\simeq" "\simeq" "\mbox{$\hspace{.29ex}\simeq\hspace{.29ex}$}" |
|
319 |
> "<=" "<=" "\mbox{$\hspace{.29ex}\le\hspace{.29ex}$}" |
|
4639 | 320 |
> "::" "::" "\mbox{$:\hspace{-.07ex}:$}" #"\mbox{$\hspace{-.1ex}:\hspace{-.07ex}:\hspace{.1ex}$}" |
1826 | 321 |
|
322 |
# arrows, Pure, HOL |
|
323 |
> "<-" "<-" "\mbox{$\leftarrow$}" |
|
324 |
> "-@@@@@" "-" "\mbox{$-$}" |
|
325 |
> "->" "->" "\mbox{$\rightarrow$}" |
|
4172 | 326 |
> "\\Leftarrow" "<=" "\mbox{$\Leftarrow$}" |
1826 | 327 |
> "=@@@@@" "=" "\mbox{$=$}" |
4172 | 328 |
> "=>" "=>" "\mbox{$\hspace{.12ex}\Rightarrow$}" |
329 |
> "\\frown" "\frown" "\mbox{$\frown$}" |
|
330 |
> "\\mapsto" "|->" "\mbox{$\mapsto$}" |
|
331 |
> "\\leadsto" "~>" "\mbox{$\hspace{.05ex}\leadsto$}" |
|
332 |
> "\\uparrow" "\uparrow" "\mbox{$\uparrow$}" |
|
333 |
> "\\downarrow" "\downarrow" "\mbox{$\downarrow$}" |
|
1826 | 334 |
> "~:" "~:" "\mbox{$\notin$}" |
335 |
||
336 |
# arithmetic, HOLCF |
|
4172 | 337 |
> "\\times" "*" "\mbox{$\hspace{-.29ex}\times\hspace{-.29ex}$}" |
338 |
> "\\oplus" "++" "\mbox{$\hspace{.29ex}\oplus\hspace{.29ex}$}" #\varoplus |
|
339 |
> "\\ominus" "--" "\mbox{$\hspace{.29ex}\ominus\hspace{.29ex}$}" #\varominus |
|
340 |
> "\\otimes" "**" "\mbox{$\hspace{.29ex}\otimes\hspace{.29ex}$}" #\varotimes |
|
341 |
> "\\oslash" "//" "\mbox{$\hspace{.29ex}\oslash\hspace{.29ex}$}" #\varoslash |
|
342 |
> "\\subset" "\subset" "\mbox{$\subset$}" |
|
343 |
> "\\infty" "\infty" "\mbox{$\infty$}" |
|
1826 | 344 |
|
345 |
# misc |
|
4172 | 346 |
> "\\Box" "\Box" "\mbox{$\Box$}" |
347 |
> "\\Diamond" "<>" "\mbox{$\hspace{.29ex}\Diamond\hspace{.29ex}$}" |
|
348 |
> "\\circ" " o " "\mbox{$\circ$}" |
|
349 |
> "\\bullet" "\bullet" "\mbox{$\bullet$}" |
|
1826 | 350 |
> "\|\|" "||" "\mbox{$\parallel$}" |
4172 | 351 |
> "\\tick" "\tick" "\mbox{$\surd$}" |
352 |
> "\\filter" "\filter" "\mbox{\copyright}" |
|
1826 | 353 |
END_HI_TABLE |
354 |
||
355 |
############################################################ |
|
356 |
# Setup for translationTableSeq in file conv-tables.h |
|
357 |
# and lexer source conv-lex.x |
|
358 |
# |
|
359 |
# Keyword for the being of the table is BEGIN_SEQ_TABLE |
|
360 |
# Keyword for the end of the table is END_SEQ_TABLE |
|
361 |
# |
|
362 |
# Lines beginning with # are ignored as everywhere in this file. |
|
363 |
# Lines obeying the syntax given below are treated as table entries. |
|
364 |
# All other lines are ignored, too. This is for comments. |
|
365 |
# |
|
366 |
# Syntax of a table entry: |
|
367 |
# |
|
368 |
# > "lex expr 8bit" "lex expr ascii" "ascii replace" "LaTeX replace" anything |
|
369 |
# |
|
370 |
# The double quotes enclose the lex expressions, the ascii replacement, and |
|
371 |
# the LaTeX replacement in pure lex rsp. pure ascii rsp. LaTeX syntax. |
|
372 |
# |
|
373 |
# The strings for the lex expressions are literally passed to lex. Backslashes |
|
374 |
# are not duplicated! |
|
375 |
# Every \ in the replacements except when used for hex-notation \x?? is |
|
376 |
# automatically duplicated by the script! The strings are used in |
|
377 |
# printf output statements in the C code. |
|
378 |
# |
|
379 |
# Attention: you have to use hex-notation \x22 to produce a " inside |
|
380 |
# the double quoted strings. An explicit " will terminate the string. |
|
381 |
# |
|
382 |
# The following `anything' is ignored by the perl script. |
|
383 |
# This is for comments. |
|
384 |
# |
|
385 |
# The ordering of entries in table SEQ_TABLE is irrelevant! |
|
386 |
# Empty table is allowed. |
|
387 |
# |
|
388 |
||
389 |
BEGIN_SEQ_TABLE |
|
390 |
||
391 |
# Pure |
|
4172 | 392 |
> "êë" "==>" "==>" "\mbox{$\hspace{-.083ex}\Longrightarrow$}" |
1826 | 393 |
|
394 |
# HOL |
|
395 |
> "çè" "-->" "-->" "\mbox{$\longrightarrow$}" |
|
4172 | 396 |
> "Ã!" "\?!" "?!" "\mbox{$\exists_1$}" |
397 |
> "ALL@@@@@" "ALL\ " "ALL " "\mbox{$\forall$}" |
|
398 |
> "EX@@@@@" "EX\ " "EX " "\mbox{$\exists$}" |
|
1826 | 399 |
|
400 |
#HOLCF |
|
4773
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4639
diff
changeset
|
401 |
> "<<\|" "@<<\|" "<<|" "\mbox{$\ll\!\mid$}" |
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4639
diff
changeset
|
402 |
> "<\|" "@<\|" "<|" "\mbox{$<\!\mid$}" |
1826 | 403 |
|
404 |
# misc ? |
|
405 |
> "éê" "<==" "<==" "\mbox{$\Longleftarrow$}" |
|
406 |
> "éë" "<=>" "<=>" "\mbox{$\Leftrightarrow$}" |
|
407 |
> "æç" "<--" "<--" "\mbox{$\longleftarrow$}" |
|
4639 | 408 |
> "æè" "<->" "<->" "\mbox{$\leftrightarrow$}" |
4773
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4639
diff
changeset
|
409 |
#> "\^-1" "@\^-1" "^-1" "\mbox{$^{\tt -1}$}" |
4172 | 410 |
|
411 |
#Isabelle |
|
4773
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4639
diff
changeset
|
412 |
> "^arities" "^@arities" "arities" "\mbox{\bf arities}" |
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4639
diff
changeset
|
413 |
> "^axclass" "^@axclass" "axclass" "\mbox{\bf axclass}" |
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4639
diff
changeset
|
414 |
> "^constdefs" "^@constdefs" "constdefs" "\mbox{\bf constdefs}" |
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4639
diff
changeset
|
415 |
> "^consts" "^@consts" "consts" "\mbox{\bf consts}" |
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4639
diff
changeset
|
416 |
> "^datatype" "^@datatype" "datatype" "\mbox{\bf datatype}" |
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4639
diff
changeset
|
417 |
> "^defs" "^@defs" "defs" "\mbox{\bf defs}" |
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4639
diff
changeset
|
418 |
> "^domain" "^@domain" "domain" "\mbox{\bf domain}" |
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4639
diff
changeset
|
419 |
> "^end" "^@end" "end" "\mbox{\bf end}" |
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4639
diff
changeset
|
420 |
> "^inductive" "^@inductive" "inductive" "\mbox{\bf inductive}" |
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4639
diff
changeset
|
421 |
> "^instance" "^@instance" "instance" "\mbox{\bf instance}" |
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4639
diff
changeset
|
422 |
> "^primrec" "^@primrec" "primrec" "\mbox{\bf primrec}" |
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4639
diff
changeset
|
423 |
> "^recdef" "^@recdef" "recdef" "\mbox{\bf recdef}" |
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4639
diff
changeset
|
424 |
> "^rules" "^@rules" "rules" "\mbox{\bf rules}" |
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4639
diff
changeset
|
425 |
> "^syntax" "^@syntax" "syntax" "\mbox{\bf syntax}" |
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4639
diff
changeset
|
426 |
> "^translations""^@translations""translations""\mbox{\bf translations}" |
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4639
diff
changeset
|
427 |
> "^typedef" "^@typedef" "typedef" "\mbox{\bf typedef}" |
b6729feb8a5d
improved \tt appearance of many ASCII special symbols like #
oheimb
parents:
4639
diff
changeset
|
428 |
> "^types" "^@types" "types" "\mbox{\bf types}" |
1826 | 429 |
END_SEQ_TABLE |
4172 | 430 |
|
431 |