lib/fonts/isacr14.bdf
author wenzelm
Fri, 21 Feb 1997 15:15:26 +0100
changeset 2670 009798ca267b
parent 2298 df82271be07b
child 2674 4385d521a691
permissions -rw-r--r--
removed empty line (which broke xfedor);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2298
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
     1
STARTFONT 2.1
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
     2
COMMENT
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
     3
COMMENT  Copyright 1984, 1987 Adobe Systems, Inc.
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
     4
COMMENT  Portions Copyright 1988 Digital Equipment Corporation
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
     5
COMMENT  Portions Copyright 1993 TU Muenchen, Germany
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
     6
COMMENT
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
     7
COMMENT  Adobe is a registered trademark of Adobe Systems, Inc.  Permission
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
     8
COMMENT  to use these trademarks is hereby granted only in association with the
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
     9
COMMENT  images described in this file.
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    10
COMMENT
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    11
COMMENT  Permission to use, copy, modify, and distribute this software and
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    12
COMMENT  its documentation for any purpose and without fee is hereby granted,
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    13
COMMENT  provided that the above copyright notices appear in all copies and
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    14
COMMENT  that both those copyright notices and this permission notice appear
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    15
COMMENT  in supporting documentation, and that the names of Adobe Systems,
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    16
COMMENT  Digital Equipment Corporation, and TU Muenchen not be used in
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    17
COMMENT  advertising or publicity pertaining to distribution of the software
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    18
COMMENT  without specific, written prior permission.  Adobe Systems, Digital
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    19
COMMENT  Equipment Corporation, and TU Muenchen  make no representations about
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    20
COMMENT  the suitability of this software for any purpose.  It is provided "as
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    21
COMMENT  is" without express or implied warranty.
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    22
COMMENT
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    23
COMMENT  ADOBE SYSTEMS, DIGITAL EQUIPMENT CORPORATION AND TU MUENCHEN DISCLAIM
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    24
COMMENT  ALL WARRANTIES WITH REGARD TO THIS SOFTWARE, INCLUDING ALL IMPLIED
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    25
COMMENT  WARRANTIES OF MERCHANTABILITY AND FITNESS, IN NO EVENT SHALL ADOBE
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    26
COMMENT  SYSTEMS, DIGITAL EQUIPMENT CORPORATION AND TU MUENCHEN BE LIABLE FOR 
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    27
COMMENT  ANY SPECIAL, INDIRECT OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    28
COMMENT  WHATSOEVE RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    29
COMMENT  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT 
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    30
COMMENT  OF OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    31
FONT -isabelle-courier-medium-r-normal--14-140-75-75-m-90-isabelle-0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    32
SIZE 14 75 75
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    33
FONTBOUNDINGBOX 9 14 4 -3
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    34
STARTPROPERTIES 22
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    35
FONTNAME_REGISTRY ""
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    36
FOUNDRY "Isabelle"
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    37
FAMILY_NAME "Courier"
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    38
WEIGHT_NAME "Medium"
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    39
SLANT "R"
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    40
SETWIDTH_NAME "Normal"
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    41
ADD_STYLE_NAME ""
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    42
PIXEL_SIZE 14
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    43
POINT_SIZE 140
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    44
RESOLUTION_X 75
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    45
RESOLUTION_Y 75
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    46
SPACING "M"
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    47
AVERAGE_WIDTH 90
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    48
CHARSET_REGISTRY "Isabelle"
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    49
CHARSET_ENCODING "0"
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    50
CHARSET_COLLECTIONS ""
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    51
FULL_NAME "Courier"
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    52
COPYRIGHT "Copyright (c) 1985,1987 Adobe Systems,Inc.,Portions Copyright 1988 Digital Equipment Corp., Portions Copyright 1993 TU Muenchen"
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    53
FONT_ASCENT 11
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    54
FONT_DESCENT 3
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    55
CAP_HEIGHT 9
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    56
X_HEIGHT 7
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    57
ENDPROPERTIES
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    58
CHARS 191
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    59
STARTCHAR space
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    60
ENCODING 32
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    61
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    62
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    63
BBX 1 1 0 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    64
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    65
00
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    66
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    67
STARTCHAR exclam
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    68
ENCODING 33
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    69
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    70
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    71
BBX 1 10 3 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    72
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    73
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    74
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    75
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    76
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    77
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    78
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    79
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    80
00
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    81
00
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    82
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    83
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    84
STARTCHAR quotedbl
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    85
ENCODING 34
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    86
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    87
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    88
BBX 4 4 2 5
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    89
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    90
90
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    91
90
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    92
90
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    93
90
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    94
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    95
STARTCHAR numbersign
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    96
ENCODING 35
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    97
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    98
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
    99
BBX 5 9 2 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   100
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   101
50
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   102
50
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   103
50
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   104
f8
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   105
50
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   106
f8
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   107
50
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   108
50
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   109
50
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   110
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   111
STARTCHAR dollar
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   112
ENCODING 36
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   113
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   114
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   115
BBX 5 13 2 -2
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   116
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   117
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   118
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   119
78
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   120
88
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   121
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   122
c0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   123
30
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   124
08
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   125
88
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   126
f0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   127
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   128
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   129
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   130
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   131
STARTCHAR percent
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   132
ENCODING 37
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   133
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   134
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   135
BBX 7 10 1 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   136
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   137
60
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   138
90
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   139
90
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   140
66
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   141
18
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   142
30
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   143
cc
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   144
12
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   145
12
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   146
0c
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   147
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   148
STARTCHAR ampersand
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   149
ENCODING 38
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   150
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   151
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   152
BBX 6 8 1 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   153
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   154
38
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   155
48
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   156
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   157
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   158
a8
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   159
90
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   160
98
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   161
64
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   162
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   163
STARTCHAR quoteright
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   164
ENCODING 39
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   165
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   166
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   167
BBX 3 4 2 5
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   168
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   169
60
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   170
60
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   171
c0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   172
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   173
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   174
STARTCHAR parenleft
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   175
ENCODING 40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   176
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   177
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   178
BBX 3 12 3 -2
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   179
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   180
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   181
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   182
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   183
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   184
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   185
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   186
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   187
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   188
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   189
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   190
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   191
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   192
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   193
STARTCHAR parenright
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   194
ENCODING 41
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   195
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   196
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   197
BBX 3 12 2 -2
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   198
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   199
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   200
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   201
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   202
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   203
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   204
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   205
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   206
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   207
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   208
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   209
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   210
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   211
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   212
STARTCHAR asterisk
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   213
ENCODING 42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   214
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   215
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   216
BBX 5 6 1 3
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   217
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   218
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   219
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   220
f8
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   221
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   222
50
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   223
88
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   224
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   225
STARTCHAR plus
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   226
ENCODING 43
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   227
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   228
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   229
BBX 7 7 1 1
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   230
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   231
10
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   232
10
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   233
10
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   234
fe
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   235
10
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   236
10
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   237
10
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   238
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   239
STARTCHAR comma
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   240
ENCODING 44
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   241
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   242
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   243
BBX 3 4 2 -2
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   244
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   245
60
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   246
60
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   247
c0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   248
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   249
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   250
STARTCHAR minus
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   251
ENCODING 45
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   252
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   253
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   254
BBX 7 1 1 4
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   255
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   256
fe
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   257
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   258
STARTCHAR period
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   259
ENCODING 46
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   260
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   261
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   262
BBX 2 2 3 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   263
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   264
c0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   265
c0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   266
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   267
STARTCHAR slash
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   268
ENCODING 47
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   269
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   270
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   271
BBX 6 11 1 -1
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   272
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   273
04
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   274
08
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   275
08
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   276
10
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   277
10
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   278
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   279
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   280
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   281
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   282
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   283
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   284
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   285
STARTCHAR zero
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   286
ENCODING 48
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   287
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   288
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   289
BBX 6 10 1 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   290
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   291
78
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   292
84
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   293
84
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   294
84
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   295
84
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   296
84
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   297
84
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   298
84
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   299
84
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   300
78
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   301
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   302
STARTCHAR one
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   303
ENCODING 49
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   304
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   305
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   306
BBX 5 10 1 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   307
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   308
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   309
60
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   310
a0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   311
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   312
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   313
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   314
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   315
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   316
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   317
f8
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   318
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   319
STARTCHAR two
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   320
ENCODING 50
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   321
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   322
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   323
BBX 6 10 1 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   324
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   325
78
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   326
84
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   327
84
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   328
04
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   329
08
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   330
10
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   331
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   332
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   333
84
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   334
fc
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   335
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   336
STARTCHAR three
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   337
ENCODING 51
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   338
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   339
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   340
BBX 6 10 1 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   341
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   342
78
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   343
84
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   344
04
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   345
04
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   346
38
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   347
04
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   348
04
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   349
04
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   350
84
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   351
78
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   352
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   353
STARTCHAR four
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   354
ENCODING 52
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   355
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   356
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   357
BBX 6 10 1 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   358
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   359
18
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   360
28
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   361
28
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   362
48
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   363
48
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   364
88
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   365
88
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   366
fc
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   367
08
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   368
1c
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   369
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   370
STARTCHAR five
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   371
ENCODING 53
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   372
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   373
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   374
BBX 6 10 1 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   375
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   376
7c
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   377
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   378
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   379
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   380
78
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   381
04
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   382
04
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   383
04
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   384
84
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   385
78
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   386
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   387
STARTCHAR six
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   388
ENCODING 54
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   389
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   390
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   391
BBX 6 10 1 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   392
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   393
38
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   394
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   395
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   396
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   397
b8
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   398
c4
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   399
84
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   400
84
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   401
44
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   402
38
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   403
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   404
STARTCHAR seven
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   405
ENCODING 55
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   406
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   407
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   408
BBX 6 10 1 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   409
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   410
fc
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   411
84
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   412
04
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   413
08
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   414
08
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   415
08
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   416
10
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   417
10
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   418
10
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   419
10
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   420
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   421
STARTCHAR eight
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   422
ENCODING 56
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   423
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   424
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   425
BBX 6 10 1 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   426
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   427
78
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   428
84
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   429
84
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   430
84
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   431
78
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   432
84
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   433
84
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   434
84
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   435
84
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   436
78
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   437
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   438
STARTCHAR nine
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   439
ENCODING 57
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   440
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   441
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   442
BBX 6 10 1 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   443
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   444
70
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   445
88
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   446
84
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   447
84
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   448
8c
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   449
74
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   450
04
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   451
04
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   452
08
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   453
70
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   454
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   455
STARTCHAR colon
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   456
ENCODING 58
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   457
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   458
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   459
BBX 2 7 3 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   460
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   461
c0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   462
c0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   463
00
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   464
00
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   465
00
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   466
c0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   467
c0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   468
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   469
STARTCHAR semicolon
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   470
ENCODING 59
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   471
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   472
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   473
BBX 3 9 2 -2
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   474
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   475
60
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   476
60
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   477
00
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   478
00
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   479
00
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   480
60
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   481
60
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   482
c0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   483
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   484
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   485
STARTCHAR less
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   486
ENCODING 60
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   487
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   488
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   489
BBX 7 7 1 1
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   490
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   491
06
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   492
18
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   493
60
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   494
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   495
60
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   496
18
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   497
06
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   498
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   499
STARTCHAR equal
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   500
ENCODING 61
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   501
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   502
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   503
BBX 7 3 1 3
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   504
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   505
fe
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   506
00
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   507
fe
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   508
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   509
STARTCHAR greater
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   510
ENCODING 62
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   511
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   512
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   513
BBX 7 7 1 1
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   514
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   515
c0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   516
30
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   517
0c
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   518
02
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   519
0c
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   520
30
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   521
c0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   522
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   523
STARTCHAR question
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   524
ENCODING 63
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   525
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   526
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   527
BBX 5 9 1 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   528
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   529
70
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   530
88
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   531
88
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   532
08
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   533
10
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   534
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   535
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   536
00
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   537
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   538
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   539
STARTCHAR at
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   540
ENCODING 64
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   541
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   542
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   543
BBX 7 10 1 -1
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   544
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   545
38
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   546
44
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   547
84
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   548
9c
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   549
a4
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   550
a4
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   551
9e
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   552
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   553
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   554
38
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   555
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   556
STARTCHAR A
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   557
ENCODING 65
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   558
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   559
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   560
BBX 9 9 0 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   561
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   562
3800
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   563
0800
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   564
1400
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   565
1400
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   566
2200
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   567
3e00
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   568
4100
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   569
4100
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   570
f780
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   571
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   572
STARTCHAR B
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   573
ENCODING 66
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   574
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   575
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   576
BBX 7 9 1 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   577
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   578
fc
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   579
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   580
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   581
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   582
7c
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   583
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   584
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   585
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   586
fc
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   587
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   588
STARTCHAR C
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   589
ENCODING 67
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   590
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   591
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   592
BBX 7 9 1 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   593
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   594
3a
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   595
46
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   596
82
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   597
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   598
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   599
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   600
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   601
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   602
3c
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   603
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   604
STARTCHAR D
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   605
ENCODING 68
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   606
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   607
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   608
BBX 8 9 0 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   609
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   610
fc
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   611
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   612
41
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   613
41
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   614
41
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   615
41
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   616
41
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   617
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   618
fc
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   619
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   620
STARTCHAR E
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   621
ENCODING 69
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   622
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   623
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   624
BBX 7 9 1 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   625
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   626
fe
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   627
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   628
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   629
48
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   630
78
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   631
48
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   632
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   633
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   634
fe
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   635
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   636
STARTCHAR F
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   637
ENCODING 70
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   638
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   639
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   640
BBX 7 9 1 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   641
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   642
fe
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   643
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   644
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   645
48
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   646
78
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   647
48
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   648
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   649
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   650
f0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   651
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   652
STARTCHAR G
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   653
ENCODING 71
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   654
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   655
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   656
BBX 8 9 0 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   657
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   658
3a
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   659
46
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   660
82
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   661
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   662
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   663
8f
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   664
82
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   665
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   666
3c
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   667
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   668
STARTCHAR H
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   669
ENCODING 72
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   670
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   671
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   672
BBX 8 9 0 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   673
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   674
e7
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   675
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   676
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   677
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   678
7e
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   679
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   680
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   681
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   682
e7
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   683
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   684
STARTCHAR I
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   685
ENCODING 73
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   686
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   687
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   688
BBX 5 9 2 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   689
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   690
f8
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   691
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   692
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   693
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   694
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   695
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   696
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   697
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   698
f8
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   699
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   700
STARTCHAR J
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   701
ENCODING 74
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   702
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   703
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   704
BBX 7 9 1 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   705
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   706
3e
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   707
08
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   708
08
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   709
08
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   710
08
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   711
88
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   712
88
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   713
88
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   714
70
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   715
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   716
STARTCHAR K
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   717
ENCODING 75
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   718
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   719
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   720
BBX 8 9 0 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   721
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   722
ee
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   723
44
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   724
48
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   725
50
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   726
70
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   727
48
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   728
44
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   729
44
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   730
e3
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   731
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   732
STARTCHAR L
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   733
ENCODING 76
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   734
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   735
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   736
BBX 8 9 0 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   737
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   738
f8
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   739
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   740
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   741
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   742
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   743
21
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   744
21
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   745
21
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   746
ff
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   747
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   748
STARTCHAR M
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   749
ENCODING 77
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   750
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   751
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   752
BBX 9 9 0 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   753
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   754
e380
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   755
6300
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   756
5700
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   757
5500
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   758
4900
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   759
4900
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   760
4100
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   761
4100
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   762
e380
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   763
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   764
STARTCHAR N
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   765
ENCODING 78
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   766
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   767
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   768
BBX 8 9 0 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   769
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   770
e7
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   771
62
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   772
52
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   773
52
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   774
4a
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   775
4a
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   776
46
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   777
46
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   778
e2
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   779
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   780
STARTCHAR O
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   781
ENCODING 79
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   782
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   783
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   784
BBX 8 9 0 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   785
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   786
3c
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   787
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   788
81
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   789
81
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   790
81
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   791
81
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   792
81
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   793
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   794
3c
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   795
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   796
STARTCHAR P
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   797
ENCODING 80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   798
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   799
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   800
BBX 7 9 1 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   801
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   802
fc
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   803
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   804
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   805
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   806
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   807
7c
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   808
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   809
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   810
f0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   811
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   812
STARTCHAR Q
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   813
ENCODING 81
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   814
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   815
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   816
BBX 8 11 0 -2
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   817
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   818
3c
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   819
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   820
81
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   821
81
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   822
81
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   823
81
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   824
81
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   825
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   826
3c
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   827
31
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   828
5e
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   829
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   830
STARTCHAR R
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   831
ENCODING 82
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   832
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   833
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   834
BBX 8 9 0 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   835
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   836
fc
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   837
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   838
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   839
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   840
44
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   841
78
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   842
44
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   843
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   844
e1
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   845
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   846
STARTCHAR S
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   847
ENCODING 83
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   848
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   849
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   850
BBX 6 9 1 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   851
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   852
74
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   853
8c
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   854
84
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   855
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   856
78
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   857
04
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   858
84
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   859
c4
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   860
b8
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   861
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   862
STARTCHAR T
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   863
ENCODING 84
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   864
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   865
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   866
BBX 7 9 1 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   867
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   868
fe
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   869
92
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   870
92
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   871
10
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   872
10
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   873
10
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   874
10
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   875
10
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   876
7c
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   877
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   878
STARTCHAR U
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   879
ENCODING 85
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   880
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   881
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   882
BBX 8 9 0 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   883
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   884
e7
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   885
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   886
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   887
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   888
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   889
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   890
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   891
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   892
3c
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   893
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   894
STARTCHAR V
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   895
ENCODING 86
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   896
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   897
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   898
BBX 9 9 0 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   899
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   900
e380
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   901
4100
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   902
4100
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   903
2200
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   904
2200
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   905
1400
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   906
1400
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   907
0800
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   908
0800
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   909
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   910
STARTCHAR W
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   911
ENCODING 87
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   912
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   913
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   914
BBX 9 9 0 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   915
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   916
e380
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   917
4100
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   918
4900
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   919
4900
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   920
5500
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   921
5500
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   922
2200
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   923
2200
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   924
2200
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   925
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   926
STARTCHAR X
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   927
ENCODING 88
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   928
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   929
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   930
BBX 8 9 0 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   931
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   932
e7
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   933
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   934
24
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   935
24
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   936
18
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   937
24
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   938
24
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   939
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   940
e7
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   941
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   942
STARTCHAR Y
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   943
ENCODING 89
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   944
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   945
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   946
BBX 7 9 1 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   947
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   948
ee
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   949
44
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   950
44
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   951
28
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   952
28
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   953
10
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   954
10
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   955
10
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   956
7c
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   957
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   958
STARTCHAR Z
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   959
ENCODING 90
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   960
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   961
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   962
BBX 6 9 1 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   963
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   964
fc
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   965
84
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   966
88
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   967
10
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   968
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   969
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   970
44
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   971
84
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   972
fc
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   973
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   974
STARTCHAR bracketleft
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   975
ENCODING 91
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   976
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   977
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   978
BBX 3 12 3 -2
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   979
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   980
e0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   981
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   982
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   983
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   984
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   985
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   986
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   987
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   988
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   989
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   990
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   991
e0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   992
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   993
STARTCHAR backslash
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   994
ENCODING 92
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   995
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   996
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   997
BBX 6 11 1 -1
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   998
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
   999
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1000
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1001
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1002
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1003
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1004
10
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1005
10
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1006
08
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1007
08
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1008
04
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1009
04
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1010
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1011
STARTCHAR bracketright
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1012
ENCODING 93
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1013
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1014
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1015
BBX 3 12 2 -2
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1016
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1017
e0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1018
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1019
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1020
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1021
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1022
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1023
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1024
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1025
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1026
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1027
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1028
e0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1029
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1030
STARTCHAR asciicircum
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1031
ENCODING 94
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1032
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1033
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1034
BBX 5 5 2 4
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1035
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1036
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1037
50
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1038
50
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1039
88
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1040
88
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1041
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1042
STARTCHAR underscore
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1043
ENCODING 95
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1044
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1045
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1046
BBX 9 1 0 -3
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1047
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1048
ff80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1049
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1050
STARTCHAR quoteleft
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1051
ENCODING 96
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1052
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1053
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1054
BBX 3 4 2 5
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1055
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1056
c0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1057
c0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1058
60
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1059
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1060
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1061
STARTCHAR a
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1062
ENCODING 97
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1063
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1064
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1065
BBX 7 7 1 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1066
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1067
78
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1068
84
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1069
04
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1070
7c
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1071
84
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1072
8c
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1073
76
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1074
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1075
STARTCHAR b
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1076
ENCODING 98
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1077
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1078
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1079
BBX 8 10 0 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1080
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1081
c0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1082
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1083
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1084
5c
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1085
62
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1086
41
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1087
41
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1088
41
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1089
62
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1090
dc
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1091
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1092
STARTCHAR c
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1093
ENCODING 99
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1094
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1095
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1096
BBX 7 7 1 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1097
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1098
3a
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1099
46
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1100
82
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1101
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1102
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1103
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1104
3c
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1105
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1106
STARTCHAR d
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1107
ENCODING 100
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1108
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1109
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1110
BBX 8 10 0 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1111
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1112
06
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1113
02
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1114
02
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1115
3a
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1116
46
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1117
82
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1118
82
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1119
82
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1120
46
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1121
3b
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1122
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1123
STARTCHAR e
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1124
ENCODING 101
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1125
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1126
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1127
BBX 7 7 1 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1128
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1129
38
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1130
44
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1131
82
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1132
fe
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1133
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1134
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1135
3c
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1136
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1137
STARTCHAR f
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1138
ENCODING 102
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1139
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1140
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1141
BBX 7 10 1 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1142
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1143
1e
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1144
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1145
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1146
fc
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1147
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1148
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1149
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1150
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1151
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1152
f8
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1153
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1154
STARTCHAR g
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1155
ENCODING 103
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1156
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1157
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1158
BBX 8 10 0 -3
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1159
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1160
3b
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1161
46
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1162
82
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1163
82
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1164
82
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1165
46
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1166
3a
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1167
02
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1168
04
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1169
78
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1170
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1171
STARTCHAR h
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1172
ENCODING 104
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1173
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1174
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1175
BBX 8 10 0 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1176
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1177
c0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1178
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1179
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1180
5c
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1181
62
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1182
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1183
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1184
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1185
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1186
e7
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1187
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1188
STARTCHAR i
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1189
ENCODING 105
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1190
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1191
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1192
BBX 5 10 2 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1193
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1194
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1195
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1196
00
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1197
e0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1198
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1199
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1200
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1201
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1202
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1203
f8
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1204
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1205
STARTCHAR j
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1206
ENCODING 106
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1207
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1208
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1209
BBX 5 13 1 -3
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1210
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1211
10
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1212
10
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1213
00
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1214
f8
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1215
08
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1216
08
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1217
08
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1218
08
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1219
08
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1220
08
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1221
08
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1222
10
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1223
e0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1224
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1225
STARTCHAR k
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1226
ENCODING 107
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1227
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1228
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1229
BBX 7 9 1 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1230
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1231
c0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1232
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1233
4e
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1234
48
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1235
50
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1236
60
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1237
50
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1238
48
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1239
ce
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1240
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1241
STARTCHAR l
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1242
ENCODING 108
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1243
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1244
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1245
BBX 5 9 2 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1246
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1247
e0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1248
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1249
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1250
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1251
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1252
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1253
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1254
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1255
f8
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1256
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1257
STARTCHAR m
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1258
ENCODING 109
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1259
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1260
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1261
BBX 9 7 0 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1262
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1263
db00
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1264
6d00
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1265
4900
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1266
4900
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1267
4900
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1268
4900
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1269
ed80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1270
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1271
STARTCHAR n
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1272
ENCODING 110
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1273
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1274
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1275
BBX 8 7 0 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1276
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1277
dc
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1278
62
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1279
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1280
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1281
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1282
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1283
e7
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1284
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1285
STARTCHAR o
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1286
ENCODING 111
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1287
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1288
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1289
BBX 8 7 0 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1290
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1291
3c
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1292
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1293
81
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1294
81
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1295
81
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1296
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1297
3c
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1298
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1299
STARTCHAR p
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1300
ENCODING 112
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1301
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1302
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1303
BBX 8 10 0 -3
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1304
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1305
dc
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1306
62
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1307
41
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1308
41
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1309
41
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1310
62
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1311
5c
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1312
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1313
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1314
f0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1315
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1316
STARTCHAR q
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1317
ENCODING 113
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1318
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1319
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1320
BBX 8 10 0 -3
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1321
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1322
3b
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1323
46
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1324
82
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1325
82
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1326
82
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1327
46
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1328
3a
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1329
02
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1330
02
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1331
0f
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1332
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1333
STARTCHAR r
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1334
ENCODING 114
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1335
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1336
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1337
BBX 7 7 1 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1338
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1339
cc
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1340
52
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1341
60
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1342
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1343
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1344
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1345
f0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1346
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1347
STARTCHAR s
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1348
ENCODING 115
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1349
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1350
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1351
BBX 6 7 1 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1352
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1353
7c
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1354
84
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1355
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1356
78
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1357
04
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1358
84
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1359
f8
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1360
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1361
STARTCHAR t
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1362
ENCODING 116
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1363
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1364
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1365
BBX 6 9 1 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1366
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1367
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1368
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1369
f8
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1370
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1371
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1372
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1373
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1374
44
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1375
38
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1376
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1377
STARTCHAR u
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1378
ENCODING 117
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1379
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1380
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1381
BBX 8 7 0 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1382
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1383
c6
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1384
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1385
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1386
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1387
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1388
46
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1389
3b
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1390
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1391
STARTCHAR v
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1392
ENCODING 118
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1393
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1394
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1395
BBX 8 7 0 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1396
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1397
e7
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1398
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1399
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1400
24
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1401
24
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1402
18
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1403
18
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1404
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1405
STARTCHAR w
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1406
ENCODING 119
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1407
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1408
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1409
BBX 9 7 0 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1410
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1411
e380
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1412
4100
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1413
4900
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1414
4900
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1415
2a00
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1416
3600
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1417
3600
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1418
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1419
STARTCHAR x
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1420
ENCODING 120
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1421
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1422
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1423
BBX 7 7 1 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1424
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1425
ee
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1426
44
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1427
28
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1428
10
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1429
28
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1430
44
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1431
ee
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1432
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1433
STARTCHAR y
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1434
ENCODING 121
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1435
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1436
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1437
BBX 8 10 0 -3
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1438
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1439
e7
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1440
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1441
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1442
24
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1443
24
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1444
18
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1445
08
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1446
10
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1447
10
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1448
78
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1449
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1450
STARTCHAR z
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1451
ENCODING 122
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1452
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1453
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1454
BBX 5 7 1 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1455
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1456
f8
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1457
88
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1458
10
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1459
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1460
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1461
88
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1462
f8
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1463
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1464
STARTCHAR braceleft
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1465
ENCODING 123
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1466
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1467
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1468
BBX 3 12 3 -2
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1469
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1470
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1471
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1472
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1473
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1474
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1475
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1476
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1477
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1478
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1479
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1480
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1481
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1482
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1483
STARTCHAR bar
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1484
ENCODING 124
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1485
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1486
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1487
BBX 1 11 4 -2
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1488
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1489
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1490
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1491
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1492
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1493
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1494
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1495
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1496
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1497
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1498
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1499
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1500
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1501
STARTCHAR braceright
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1502
ENCODING 125
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1503
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1504
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1505
BBX 3 12 2 -2
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1506
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1507
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1508
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1509
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1510
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1511
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1512
20
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1513
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1514
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1515
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1516
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1517
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1518
80
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1519
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1520
STARTCHAR asciitilde
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1521
ENCODING 126
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1522
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1523
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1524
BBX 6 2 1 3
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1525
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1526
64
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1527
98
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1528
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1529
STARTCHAR space
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1530
ENCODING 160
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1531
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1532
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1533
BBX 1 1 0 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1534
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1535
00
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1536
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1537
STARTCHAR Gamma
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1538
ENCODING 161
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1539
SWIDTH 216 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1540
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1541
BBX 7 9 1 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1542
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1543
fe
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1544
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1545
42
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1546
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1547
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1548
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1549
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1550
40
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1551
f0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1552
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1553
STARTCHAR Delta
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1554
ENCODING 162
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1555
SWIDTH 288 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1556
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1557
BBX 7 8 1 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1558
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1559
10
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1560
10
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1561
28
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1562
28
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1563
44
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1564
44
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1565
82
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1566
fe
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1567
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1568
STARTCHAR Theta
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1569
ENCODING 163
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1570
SWIDTH 264 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1571
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1572
BBX 7 9 1 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1573
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1574
38
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1575
44
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1576
82
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1577
82
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1578
fe
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1579
82
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1580
82
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1581
44
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1582
38
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1583
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1584
STARTCHAR Lambda
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1585
ENCODING 164
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1586
SWIDTH 600 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1587
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1588
BBX 9 10 0 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1589
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1590
0800
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1591
0800
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1592
1C00
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1593
3600
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1594
3600
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1595
6300
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1596
6300
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1597
C180
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1598
C180
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1599
E380
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1600
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1601
STARTCHAR Pi
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1602
ENCODING 165
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1603
SWIDTH 264 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1604
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1605
BBX 7 8 1 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1606
BITMAP
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1607
fe
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1608
44
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1609
44
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1610
44
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1611
44
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1612
44
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1613
44
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1614
ee
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1615
ENDCHAR
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1616
STARTCHAR Sigma
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1617
ENCODING 166
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1618
SWIDTH 240 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1619
DWIDTH 9 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1620
BBX 7 9 1 0
df82271be07b isabelle symbol fonts;
wenzelm
parents:
diff changeset
  1621
BITMAP