lib/fonts/IsabelleMono.sfd
author wenzelm
Fri, 22 Aug 2008 17:06:19 +0200
changeset 29073 feb740b8c043
child 29074 7250cd050f3f
permissions -rw-r--r--
Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
29073
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
     1
SplineFontDB: 2.0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
     2
FontName: IsabelleMono
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
     3
FullName: IsabelleMono
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
     4
FamilyName: IsabelleMono
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
     5
Weight: Medium
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
     6
Copyright: 
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
     7
Version: 001.000
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
     8
ItalicAngle: 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
     9
UnderlinePosition: -100
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    10
UnderlineWidth: 50
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    11
Ascent: 800
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    12
Descent: 200
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    13
NeedsXUIDChange: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    14
XUID: [1021 151 411138958 13689962]
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    15
FSType: 8
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    16
OS2Version: 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    17
OS2_WeightWidthSlopeOnly: 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    18
OS2_UseTypoMetrics: 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    19
CreationTime: 1092579958
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    20
ModificationTime: 1219416906
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    21
PfmFamily: 17
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    22
TTFWeight: 500
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    23
TTFWidth: 5
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    24
LineGap: 90
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    25
VLineGap: 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    26
Panose: 2 0 6 3 0 0 0 0 0 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    27
OS2TypoAscent: 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    28
OS2TypoAOffset: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    29
OS2TypoDescent: 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    30
OS2TypoDOffset: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    31
OS2TypoLinegap: 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    32
OS2WinAscent: 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    33
OS2WinAOffset: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    34
OS2WinDescent: 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    35
OS2WinDOffset: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    36
HheadAscent: 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    37
HheadAOffset: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    38
HheadDescent: 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    39
HheadDOffset: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    40
OS2Vendor: 'PfEd'
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    41
Lookup: 4 0 1 "'liga' Standard Ligatures lookup 0"  {"'liga' Standard Ligatures lookup 0 subtable"  } ['liga' ('DFLT' <'dflt' > ) ]
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    42
Lookup: 4 0 1 "'liga' Standard Ligatures in Latin lookup 1"  {"'liga' Standard Ligatures in Latin lookup 1 subtable"  } ['liga' ('latn' <'dflt' > ) ]
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    43
DEI: 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    44
Encoding: UnicodeFull
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    45
UnicodeInterp: none
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    46
NameList: Adobe Glyph List
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    47
DisplaySize: -48
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    48
AntiAlias: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    49
FitToEm: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    50
WinInfo: 96 16 14
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    51
BeginPrivate: 8
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    52
BlueValues 31 [-22 0 683 705 431 448 666 677]
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    53
OtherBlues 11 [-206 -194]
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    54
StdHW 4 [31]
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    55
StdVW 4 [69]
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    56
StemSnapH 7 [22 31]
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    57
StemSnapV 7 [69 89]
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    58
BlueScale 7 0.04379
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    59
ForceBold 5 false
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    60
EndPrivate
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    61
TeXData: 1 0 0 349175 174587 116391 451936 1048576 116391 783286 444596 497025 792723 393216 433062 380633 303038 157286 324010 404750 52429 2506097 1059062 262144
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    62
BeginChars: 1114112 508
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    63
StartChar: space
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    64
Encoding: 32 32 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    65
Width: 554
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    66
VWidth: 921
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    67
Flags: HW
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    68
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    69
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    70
StartChar: minute
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    71
Encoding: 8242 8242 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    72
Width: 247
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    73
Flags: W
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    74
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    75
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    76
27 486 m 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    77
 129 696 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    78
 143 725 154 735 172 735 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    79
 201 735 228 713 228 689 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    80
 228 675 223 666 208 649 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    81
 42 476 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    82
 27 486 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    83
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    84
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    85
StartChar: lessequal
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    86
Encoding: 8804 8804 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    87
Width: 777
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    88
Flags: W
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    89
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    90
HStem: -137 40<100 678>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    91
DStem: 102 325 150 346 657 63 675 98 658 630 676 595 102 368 150 346
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    92
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    93
676 595 m 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    94
 150 346 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    95
 675 98 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    96
 687 92 694 89 694 77 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    97
 694 66 685 57 674 57 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    98
 670 57 668 57 657 63 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    99
 102 325 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   100
 93 329 83 334 83 346 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   101
 83 359 92 363 102 368 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   102
 658 630 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   103
 669 636 671 636 674 636 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   104
 685 636 694 627 694 616 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   105
 694 603 686 599 676 595 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   106
661 -137 m 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   107
 116 -137 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   108
 102 -137 83 -137 83 -117 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   109
 83 -97 103 -97 117 -97 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   110
 660 -97 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   111
 675 -97 694 -97 694 -117 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   112
 694 -137 675 -137 661 -137 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   113
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   114
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   115
StartChar: fraction
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   116
Encoding: 8260 8260 3
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   117
Width: 500
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   118
Flags: W
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   119
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   120
DStem: 402 730 438 712 61 -212 97 -230
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   121
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   122
438 712 m 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   123
 97 -230 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   124
 94 -240 90 -250 76 -250 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   125
 65 -250 56 -241 56 -230 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   126
 56 -228 56 -225 61 -212 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   127
 402 730 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   128
 405 740 409 750 423 750 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   129
 434 750 443 741 443 730 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   130
 443 728 443 725 438 712 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   131
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   132
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   133
StartChar: infinity
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   134
Encoding: 8734 8734 4
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   135
Width: 1000
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   136
Flags: W
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   137
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   138
HStem: -11 32<230 251> -11 48<750 769> 410 32<743 769>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   139
VStem: 56 22<215 230> 921 22<216 237>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   140
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   141
508 272 m 1xb8
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   142
 521 294 610 442 754 442 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   143
 873 442 943 327 943 216 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   144
 943 98 867 -11 751 -11 c 0x78
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   145
 672 -11 613 31 581 58 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   146
 559 77 558 78 491 159 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   147
 478 137 389 -11 245 -11 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   148
 126 -11 56 104 56 215 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   149
 56 333 132 442 248 442 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   150
 327 442 386 400 418 373 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   151
 440 354 441 353 508 272 c 1xb8
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   152
534 237 m 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   153
 562 203 607 140 635 109 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   154
 680 60 721 37 767 37 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   155
 851 37 921 116 921 216 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   156
 921 306 867 410 761 410 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   157
 648 410 572 305 534 237 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   158
465 194 m 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   159
 437 228 392 291 364 322 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   160
 319 371 278 394 232 394 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   161
 148 394 78 315 78 215 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   162
 78 125 132 21 238 21 c 0xb8
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   163
 351 21 427 126 465 194 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   164
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   165
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   166
StartChar: florin
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   167
Encoding: 402 402 5
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   168
Width: 554
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   169
VWidth: 921
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   170
Flags: HW
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   171
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   172
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   173
540 684 m 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   174
 540 610.2 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   175
 529.2 618.6 517.65 624.975 505.35 629.325 c 128
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   176
 493.05 633.675 480.3 635.85 467.1 635.85 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   177
 436.5 635.85 412.575 626.55 395.325 607.95 c 128
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   178
 378.075 589.35 366.75 560.55 361.35 521.55 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   179
 341.1 381.6 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   180
 477.45 381.6 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   181
 477.45 317.25 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   182
 329.85 317.25 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   183
 284.85 31.5 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   184
 271.95 -48.3001 250.575 -105.45 220.725 -139.95 c 128
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   185
 190.875 -174.45 148.05 -191.7 92.25 -191.7 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   186
 75.1497 -191.7 58.9499 -190.125 43.6504 -186.975 c 128
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   187
 28.3503 -183.825 13.8001 -178.95 0 -172.35 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   188
 0 -98.5498 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   189
 14.6999 -107.85 29.5498 -114.975 44.5498 -119.925 c 128
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   190
 59.5498 -124.875 74.25 -127.35 88.6504 -127.35 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   191
 117.45 -127.35 140.925 -116.1 159.075 -93.5996 c 128
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   192
 177.225 -71.0996 190.2 -37.1999 198 8.09961 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   193
 250.65 317.25 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   194
 137.25 317.25 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   195
 137.25 381.6 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   196
 261 381.6 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   197
 283.05 530.1 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   198
 290.85 583.2 309.6 624.825 339.3 654.975 c 128
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   199
 369 685.125 406.05 700.2 450.45 700.2 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   200
 465.15 700.2 479.925 698.85 494.775 696.15 c 128
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   201
 509.625 693.45 524.7 689.4 540 684 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   202
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   203
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   204
StartChar: club
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   205
Encoding: 9827 9827 6
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   206
Width: 777
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   207
Flags: W
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   208
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   209
HStem: -22 21G<149 220 558 629>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   210
VStem: 341 96<-110 -108>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   211
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   212
490 371 m 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   213
 512 326 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   214
 526 343 556 368 604 368 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   215
 698 368 750 270 750 174 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   216
 750 68 679 -22 579 -22 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   217
 537 -22 461 -3 459 70 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   218
 409 70 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   219
 409 36 411 -18 433 -93 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   220
 437 -106 437 -108 437 -110 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   221
 437 -130 418 -130 404 -130 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   222
 374 -130 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   223
 360 -130 341 -130 341 -110 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   224
 341 -108 341 -106 344 -99 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   225
 364 -28 368 17 369 70 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   226
 319 70 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   227
 317 -3 241 -22 199 -22 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   228
 99 -22 28 68 28 174 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   229
 28 270 80 368 174 368 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   230
 222 368 253 342 267 326 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   231
 288 372 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   232
 240 409 212 470 212 532 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   233
 212 636 288 727 389 727 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   234
 489 727 566 637 566 532 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   235
 566 467 536 408 490 371 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   236
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   237
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   238
StartChar: spade
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   239
Encoding: 9824 9824 7
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   240
Width: 777
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   241
Flags: W
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   242
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   243
HStem: -22 21G<129.5 194 577 647.5>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   244
VStem: 341 96<-110 -108>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   245
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   246
404 -130 m 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   247
 374 -130 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   248
 360 -130 341 -130 341 -110 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   249
 341 -108 341 -106 344 -99 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   250
 364 -28 368 17 369 70 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   251
 319 70 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   252
 314 -22 198 -22 190 -22 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   253
 69 -22 56 133 56 203 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   254
 56 330 141 414 234 499 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   255
 307 565 340 635 369 710 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   256
 371 716 375 727 389 727 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   257
 403 727 406 718 411 705 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   258
 463 573 509 530 560 483 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   259
 653 398 722 318 722 203 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   260
 722 129 707 -22 588 -22 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   261
 566 -22 463 -15 459 70 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   262
 409 70 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   263
 409 36 411 -18 433 -93 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   264
 437 -106 437 -108 437 -110 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   265
 437 -130 418 -130 404 -130 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   266
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   267
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   268
StartChar: arrowup
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   269
Encoding: 8593 8593 8
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   270
Width: 500
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   271
Flags: W
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   272
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   273
HStem: -194 21G<240 260> 673 20G<246.5 253.5>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   274
VStem: 230 40<-177.745 609>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   275
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   276
270 609 m 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   277
 270 -161 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   278
 270 -176 270 -194 250 -194 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   279
 230 -194 230 -176 230 -161 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   280
 230 609 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   281
 170 530 89 501 84 501 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   282
 74 501 72 510 72 516 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   283
 72 528 76 530 83 533 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   284
 147 560 199 600 237 681 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   285
 241 688 243 693 250 693 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   286
 257 693 259 690 263 681 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   287
 310 579 384 547 418 532 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   288
 425 529 428 526 428 516 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   289
 428 510 426 501 416 501 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   290
 410 501 329 531 270 609 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   291
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   292
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   293
StartChar: arrowright
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   294
Encoding: 8594 8594 9
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   295
Width: 1000
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   296
Flags: W
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   297
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   298
HStem: 230 40<72.255 857>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   299
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   300
858 230 m 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   301
 89 230 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   302
 74 230 56 230 56 250 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   303
 56 270 74 270 89 270 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   304
 858 270 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   305
 783 325 750 408 750 416 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   306
 750 425 758 428 765 428 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   307
 776 428 778 423 782 414 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   308
 823 322 881 285 935 260 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   309
 936 260 942 257 942 250 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   310
 942 243 940 242 928 236 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   311
 828 189 796 116 781 82 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   312
 779 78 777 72 765 72 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   313
 758 72 750 75 750 84 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   314
 750 92 783 175 858 230 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   315
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   316
Ligature2: "'liga' Standard Ligatures in Latin lookup 1 subtable" f f
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   317
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   318
StartChar: arrowdown
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   319
Encoding: 8595 8595 10
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   320
Width: 500
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   321
Flags: W
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   322
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   323
HStem: -193 21G<246.5 252> -21 20G<79 87 413.5 421> 674 20G<240 260>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   324
VStem: 230 40<-109 672>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   325
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   326
270 661 m 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   327
 270 -109 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   328
 330 -30 411 -1 416 -1 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   329
 426 -1 428 -10 428 -16 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   330
 428 -28 424 -30 417 -33 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   331
 324 -73 287 -129 260 -187 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   332
 258 -192 254 -193 250 -193 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   333
 243 -193 241 -188 237 -181 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   334
 192 -86 131 -54 82 -32 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   335
 75 -29 72 -26 72 -16 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   336
 72 -10 74 -1 84 -1 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   337
 90 -1 171 -31 230 -109 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   338
 230 661 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   339
 230 676 230 694 250 694 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   340
 270 694 270 676 270 661 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   341
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   342
Ligature2: "'liga' Standard Ligatures in Latin lookup 1 subtable" f i
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   343
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   344
StartChar: degree
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   345
Encoding: 176 176 11
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   346
Width: 400
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   347
Flags: W
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   348
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   349
HStem: 380 57<200 211> 629 57<193 211>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   350
VStem: 50 56<523 541> 293 57<533 541>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   351
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   352
203 686 m 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   353
 286 686 350 619 350 533 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   354
 350 447 284 380 200 380 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   355
 116 380 50 448 50 534 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   356
 50 619 118 686 203 686 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   357
202 629 m 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   358
 148 629 106 586 106 533 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   359
 106 480 149 437 200 437 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   360
 252 437 293 479 293 533 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   361
 293 586 252 629 202 629 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   362
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   363
LCarets2: 1 0 
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   364
Ligature2: "'liga' Standard Ligatures in Latin lookup 1 subtable" f l
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   365
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   366
StartChar: plusminus
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   367
Encoding: 177 177 12
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   368
Width: 777
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   369
Flags: W
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   370
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   371
HStem: 0 40<72.6953 369 409 697> 313 40<72.6953 369 409 697> 646 20G<379 399>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   372
VStem: 369 40<39 313 352 641>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   373
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   374
409 313 m 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   375
 409 40 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   376
 688 40 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   377
 702 40 721 40 721 20 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   378
 721 0 702 0 688 0 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   379
 89 0 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   380
 75 0 56 0 56 20 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   381
 56 40 75 40 89 40 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   382
 369 40 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   383
 369 313 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   384
 89 313 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   385
 75 313 56 313 56 333 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   386
 56 353 75 353 89 353 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   387
 369 353 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   388
 369 634 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   389
 369 648 369 666 389 666 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   390
 409 666 409 645 409 630 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   391
 409 353 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   392
 688 353 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   393
 702 353 721 353 721 333 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   394
 721 313 702 313 688 313 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   395
 409 313 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   396
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   397
Ligature2: "'liga' Standard Ligatures in Latin lookup 1 subtable" ff i
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   398
Ligature2: "'liga' Standard Ligatures in Latin lookup 1 subtable" f f i
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   399
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   400
StartChar: second
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   401
Encoding: 8243 8243 13
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   402
Width: 411
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   403
Flags: W
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   404
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   405
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   406
20 486 m 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   407
 122 696 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   408
 136 725 147 735 165 735 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   409
 194 735 221 713 221 689 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   410
 221 675 216 666 201 649 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   411
 35 476 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   412
 20 486 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   413
212 486 m 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   414
 314 696 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   415
 328 725 339 735 357 735 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   416
 386 735 413 713 413 689 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   417
 413 675 408 666 393 649 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   418
 227 476 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   419
 212 486 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   420
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   421
Ligature2: "'liga' Standard Ligatures in Latin lookup 1 subtable" ff l
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   422
Ligature2: "'liga' Standard Ligatures in Latin lookup 1 subtable" f f l
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   423
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   424
StartChar: greaterequal
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   425
Encoding: 8805 8805 14
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   426
Width: 777
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   427
Flags: W
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   428
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   429
HStem: -137 40<100 677>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   430
DStem: 102 595 121 629 627 347 675 368 627 347 675 325 101 98 120 63
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   431
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   432
675 325 m 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   433
 120 63 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   434
 109 57 107 57 103 57 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   435
 92 57 83 66 83 77 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   436
 83 90 92 94 101 98 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   437
 627 347 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   438
 102 595 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   439
 89 601 83 604 83 616 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   440
 83 627 92 636 103 636 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   441
 106 636 108 636 121 629 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   442
 675 368 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   443
 685 363 694 359 694 346 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   444
 694 334 684 329 675 325 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   445
661 -137 m 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   446
 116 -137 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   447
 102 -137 83 -137 83 -117 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   448
 83 -97 103 -97 117 -97 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   449
 660 -97 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   450
 675 -97 694 -97 694 -117 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   451
 694 -137 675 -137 661 -137 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   452
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   453
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   454
StartChar: multiply
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   455
Encoding: 215 215 15
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   456
Width: 777
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   457
Flags: W
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   458
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   459
DStem: 160 450 188 478 588 22 617 50 589 478 617 450 160 51 188 22
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   460
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   461
418 250 m 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   462
 617 50 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   463
 628 39 630 37 630 29 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   464
 630 18 622 9 610 9 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   465
 604 9 598 12 588 22 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   466
 388 222 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   467
 188 22 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   468
 177 11 175 9 167 9 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   469
 157 9 147 18 147 29 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   470
 147 35 150 41 160 51 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   471
 359 250 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   472
 160 450 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   473
 151 459 147 463 147 471 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   474
 147 482 157 491 167 491 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   475
 175 491 177 489 188 478 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   476
 389 278 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   477
 589 478 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   478
 598 487 602 491 610 491 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   479
 621 491 630 482 630 471 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   480
 630 463 628 461 617 450 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   481
 418 250 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   482
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   483
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   484
StartChar: proportional
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   485
Encoding: 8733 8733 16
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   486
Width: 777
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   487
Flags: W
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   488
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   489
HStem: -11 29<215 232> -11 41<684 699> 413 29<679 701>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   490
VStem: 56 22<215 237>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   491
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   492
485 235 m 1xb0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   493
 528 170 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   494
 565 112 618 30 699 30 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   495
 704 30 716 32 722 33 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   496
 722 -7 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   497
 721 -7 705 -11 686 -11 c 0x70
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   498
 564 -11 496 94 453 161 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   499
 418 87 342 -11 228 -11 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   500
 115 -11 56 106 56 215 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   501
 56 331 121 442 230 442 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   502
 352 442 420 337 463 270 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   503
 498 344 574 442 688 442 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   504
 691 442 710 442 719 439 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   505
 721 437 722 436 722 410 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   506
 711 413 700 413 695 413 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   507
 583 413 515 302 485 235 c 1xb0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   508
431 196 m 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   509
 388 261 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   510
 351 319 298 401 217 401 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   511
 135 401 78 315 78 215 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   512
 78 122 125 18 221 18 c 0xb0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   513
 333 18 401 129 431 196 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   514
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   515
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   516
StartChar: partialdiff
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   517
Encoding: 8706 8706 17
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   518
Width: 530
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   519
Flags: W
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   520
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   521
HStem: -22 28<215 233> 435 22<334 352> 523 88<197 206> 691 25<332 361>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   522
VStem: 40 77<119 156> 159 92<558 576> 491 75<457 510>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   523
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   524
463 339 m 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   525
 464 339 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   526
 485 420 491 471 491 510 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   527
 491 639 421 691 348 691 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   528
 319 691 248 685 204 611 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   529
 220 611 251 611 251 576 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   530
 251 553 230 523 197 523 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   531
 167 523 159 544 159 558 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   532
 159 586 205 716 350 716 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   533
 473 716 566 616 566 457 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   534
 566 314 462 -22 224 -22 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   535
 84 -22 40 94 40 156 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   536
 40 187 47 280 130 363 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   537
 208 441 273 457 334 457 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   538
 412 457 453 401 463 339 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   539
227 6 m 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   540
 381 6 445 231 445 303 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   541
 445 323 443 435 334 435 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   542
 272 435 223 403 183 346 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   543
 142 286 117 146 117 119 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   544
 117 109 117 6 227 6 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   545
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   546
Ligature2: "'liga' Standard Ligatures lookup 0 subtable" space acutecomb
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   547
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   548
StartChar: bullet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   549
Encoding: 8226 8226 18
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   550
Width: 500
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   551
Flags: W
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   552
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   553
HStem: 424 20G<195.5 302.5>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   554
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   555
443 250 m 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   556
 443 145 358 56 249 56 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   557
 144 56 56 143 56 250 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   558
 56 355 141 444 250 444 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   559
 355 444 443 357 443 250 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   560
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   561
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   562
StartChar: divide
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   563
Encoding: 247 247 19
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   564
Width: 777
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   565
Flags: W
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   566
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   567
HStem: -30 128<378.065 392> 230 40<72.6953 697> 402 128<378.065 392>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   568
VStem: 325 128<22.9763 37 454.976 469>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   569
CounterMasks: 1 00
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   570
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   571
453 466 m 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   572
 453 430 423 402 389 402 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   573
 355 402 325 431 325 466 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   574
 325 502 355 530 389 530 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   575
 423 530 453 501 453 466 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   576
453 34 m 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   577
 453 -2 423 -30 389 -30 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   578
 355 -30 325 -1 325 34 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   579
 325 70 355 98 389 98 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   580
 423 98 453 69 453 34 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   581
89 270 m 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   582
 689 270 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   583
 703 270 722 270 722 250 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   584
 722 230 703 230 689 230 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   585
 89 230 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   586
 75 230 56 230 56 250 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   587
 56 270 75 270 89 270 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   588
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   589
Ligature2: "'liga' Standard Ligatures lookup 0 subtable" space uni0306
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   590
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   591
StartChar: notequal
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   592
Encoding: 8800 8800 20
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   593
Width: 777
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   594
Flags: W
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   595
Validated: 5
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   596
HStem: 133 40<72.943 297 90 697> 327 40<72.943 393 89 697>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   597
DStem: 596 698 631 678 146 -178 181 -198
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   598
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   599
631 678 m 6
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   600
 181 -198 l 6
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   601
 175 -210 169 -216 159 -216 c 4
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   602
 145 -216 139 -203 139 -196 c 4
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   603
 139 -192 140 -190 146 -178 c 6
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   604
 596 698 l 6
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   605
 602 710 608 716 618 716 c 4
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   606
 632 716 638 703 638 696 c 4
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   607
 638 692 637 690 631 678 c 6
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   608
687 327 m 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   609
 90 327 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   610
 75 327 56 327 56 347 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   611
 56 367 75 367 89 367 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   612
 688 367 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   613
 702 367 721 367 721 347 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   614
 721 327 702 327 687 327 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   615
688 133 m 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   616
 89 133 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   617
 75 133 56 133 56 153 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   618
 56 173 75 173 90 173 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   619
 687 173 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   620
 702 173 721 173 721 153 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   621
 721 133 702 133 688 133 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   622
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   623
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   624
StartChar: equivalence
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   625
Encoding: 8801 8801 21
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   626
Width: 777
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   627
Flags: W
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   628
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   629
HStem: 36 40<72.943 697> 230 40<72.6953 697> 424 40<72.943 697>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   630
CounterMasks: 1 00
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   631
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   632
687 424 m 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   633
 90 424 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   634
 75 424 56 424 56 444 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   635
 56 464 75 464 89 464 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   636
 688 464 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   637
 702 464 721 464 721 444 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   638
 721 424 702 424 687 424 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   639
688 36 m 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   640
 89 36 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   641
 75 36 56 36 56 56 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   642
 56 76 75 76 90 76 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   643
 687 76 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   644
 702 76 721 76 721 56 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   645
 721 36 702 36 688 36 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   646
688 230 m 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   647
 89 230 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   648
 75 230 56 230 56 250 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   649
 56 270 75 270 89 270 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   650
 688 270 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   651
 702 270 721 270 721 250 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   652
 721 230 702 230 688 230 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   653
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   654
LCarets2: 1 0 
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   655
Ligature2: "'liga' Standard Ligatures lookup 0 subtable" space uni030A
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   656
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   657
StartChar: approxequal
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   658
Encoding: 8776 8776 22
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   659
Width: 777
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   660
Flags: W
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   661
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   662
HStem: 56 56<536.126 569> 194 56<222 233> 289 56<536.126 569> 427 56<222 233>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   663
VStem: 56 28<78 87 311 320>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   664
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   665
721 452 m 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   666
 721 359 647 289 555 289 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   667
 491 289 438 324 395 352 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   668
 327 397 282 427 222 427 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   669
 172 427 89 397 84 313 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   670
 84 308 81 290 70 290 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   671
 63 290 56 298 56 320 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   672
 56 413 130 483 222 483 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   673
 286 483 339 448 382 420 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   674
 450 375 495 345 555 345 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   675
 619 345 689 387 693 455 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   676
 694 465 697 482 707 482 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   677
 714 482 721 473 721 452 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   678
721 218 m 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   679
 721 129 649 56 555 56 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   680
 491 56 438 91 395 119 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   681
 327 164 282 194 222 194 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   682
 172 194 89 164 84 80 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   683
 84 75 81 57 70 57 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   684
 63 57 56 65 56 87 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   685
 56 180 130 250 222 250 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   686
 286 250 339 215 382 187 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   687
 450 142 495 112 555 112 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   688
 626 112 688 160 693 217 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   689
 694 232 696 249 707 249 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   690
 714 249 721 239 721 218 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   691
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   692
LCarets2: 1 0 
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   693
Ligature2: "'liga' Standard Ligatures lookup 0 subtable" space uni0327
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   694
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   695
StartChar: ellipsis
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   696
Encoding: 8230 8230 23
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   697
Width: 1000
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   698
Flags: W
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   699
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   700
HStem: -13 21G<151.5 182.5 484.5 515.5 817.5 848.5>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   701
VStem: 111 112<44 52> 444 112<44 52> 777 112<44 52>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   702
CounterMasks: 1 00
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   703
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   704
168 100 m 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   705
 197 100 223 74 223 44 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   706
 223 13 198 -13 167 -13 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   707
 136 -13 111 13 111 44 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   708
 111 75 137 100 168 100 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   709
501 100 m 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   710
 530 100 556 74 556 44 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   711
 556 13 531 -13 500 -13 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   712
 469 -13 444 13 444 44 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   713
 444 75 470 100 501 100 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   714
834 100 m 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   715
 863 100 889 74 889 44 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   716
 889 13 864 -13 833 -13 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   717
 802 -13 777 13 777 44 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   718
 777 75 803 100 834 100 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   719
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   720
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   721
StartChar: uniF8E6
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   722
Encoding: 63718 63718 24
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   723
Width: 603
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   724
Flags: W
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   725
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   726
VStem: 280 56<-120 1010>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   727
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   728
336 1010 m 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   729
 336 -120 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   730
 280 -120 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   731
 280 1010 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   732
 336 1010 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   733
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   734
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   735
StartChar: uniF8E7
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   736
Encoding: 63719 63719 25
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   737
Width: 1000
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   738
Flags: W
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   739
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   740
HStem: 220 56<-60 1050>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   741
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   742
-60 220 m 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   743
 -60 276 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   744
 1050 276 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   745
 1050 220 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   746
 -60 220 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   747
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   748
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   749
StartChar: carriagereturn
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   750
Encoding: 8629 8629 26
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   751
Width: 658
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   752
Flags: W
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   753
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   754
HStem: 68 56<184 602>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   755
VStem: 547 55<124 629>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   756
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   757
602 68 m 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   758
 185 68 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   759
 185 -16 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   760
 15 96 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   761
 185 208 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   762
 185 124 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   763
 547 124 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   764
 547 629 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   765
 602 629 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   766
 602 68 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   767
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   768
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   769
StartChar: aleph
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   770
Encoding: 8501 8501 27
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   771
Width: 611
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   772
Flags: W
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   773
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   774
HStem: 0 22<70 81> 673 20G<79.5 86.5 411.5 416>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   775
VStem: 83 67<237 257> 143 97<50.9253 67> 518 36<14 64>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   776
DStem: 187 436 137 587 473 107 417 265
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   777
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   778
137 587 m 2xe8
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   779
 417 265 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   780
 420 293 428 341 434 376 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   781
 437 391 452 474 455 522 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   782
 388 586 388 609 388 630 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   783
 388 681 409 693 414 693 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   784
 418 693 421 691 423 688 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   785
 428 672 431 664 465 611 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   786
 486 577 488 575 518 548 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   787
 554 514 554 491 554 474 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   788
 554 420 533 410 528 410 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   789
 520 410 519 417 518 422 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   790
 517 436 515 457 484 493 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   791
 480 455 467 386 464 367 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   792
 447 275 446 242 446 239 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   793
 446 232 446 230 461 213 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   794
 554 108 554 92 554 64 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   795
 554 13 533 1 528 1 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   796
 519 1 518 9 518 14 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   797
 517 26 515 59 473 107 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   798
 187 436 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   799
 154 367 150 279 150 248 c 0xe8
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   800
 150 213 155 201 196 151 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   801
 215 128 240 97 240 60 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   802
 240 10 187 0 141 0 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   803
 81 0 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   804
 64 0 56 0 56 11 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   805
 56 22 63 22 72 22 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   806
 143 24 143 50 143 61 c 0xd8
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   807
 143 82 135 105 115 142 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   808
 88 192 83 215 83 241 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   809
 83 326 133 415 164 461 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   810
 115 522 126 505 103 534 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   811
 56 594 56 609 56 630 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   812
 56 681 77 693 82 693 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   813
 91 693 92 685 92 680 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   814
 93 668 95 635 137 587 c 2xe8
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   815
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   816
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   817
StartChar: Ifraktur
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   818
Encoding: 8465 8465 28
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   819
Width: 722
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   820
Flags: W
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   821
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   822
HStem: -11 23<415 425> 409 22<570 584> 475 22<572 584> 683 22<263 281>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   823
VStem: 56 31<515 517> 449 83<308 327> 541 83<139 150>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   824
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   825
287 336 m 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   826
 287 325 279 325 270 325 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   827
 179 325 56 391 56 515 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   828
 56 624 155 705 273 705 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   829
 369 705 479 654 542 538 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   830
 559 505 563 497 582 497 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   831
 586 497 654 497 662 546 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   832
 663 554 665 558 677 558 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   833
 684 558 693 558 693 545 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   834
 693 504 644 475 580 475 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   835
 495 475 447 535 406 587 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   836
 363 642 330 683 270 683 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   837
 176 683 87 613 87 515 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   838
 87 436 151 354 271 347 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   839
 280 346 287 346 287 336 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   840
81 183 m 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   841
 124 183 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   842
 193 183 235 150 300 88 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   843
 362 30 402 12 419 12 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   844
 442 12 541 49 541 139 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   845
 541 168 525 190 498 220 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   846
 463 259 449 283 449 316 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   847
 449 382 509 431 578 431 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   848
 646 431 693 385 693 340 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   849
 693 329 688 326 677 326 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   850
 667 326 663 329 662 337 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   851
 654 409 582 409 580 409 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   852
 536 409 532 344 532 320 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   853
 532 300 532 283 570 240 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   854
 598 208 624 179 624 139 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   855
 624 132 624 77 573 33 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   856
 521 -11 468 -11 417 -11 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   857
 340 -11 316 -11 215 81 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   858
 165 126 126 156 76 161 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   859
 61 162 56 162 56 172 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   860
 56 183 64 183 81 183 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   861
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   862
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   863
StartChar: Rfraktur
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   864
Encoding: 8476 8476 29
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   865
Width: 722
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   866
Flags: W
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   867
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   868
HStem: -22 22<189 196> 94 27<98 110> 243 22<107 123> 345 31<342 457> 678 38<487 549> 683 22<157 175>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   869
VStem: 63 27<114 118> 162 32<374 398> 260 83<209 344 209 475> 467 87<93 105.835 93 127>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   870
DStem: 496 668 572 703 624 439 708 459 640 46 685 44 596 11 617 -8
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   871
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   872
572 703 m 2xfbc0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   873
 708 459 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   874
 714 448 714 446 714 445 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   875
 714 439 712 437 706 434 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   876
 589 366 563 358 541 352 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   877
 544 306 554 164 554 127 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   878
 554 116 550 108 550 93 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   879
 550 51 576 23 596 11 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   880
 640 46 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   881
 654 58 679 77 683 77 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   882
 685 77 702 72 702 62 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   883
 702 59 701 58 685 44 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   884
 662 27 640 9 617 -8 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   885
 598 -22 596 -22 583 -22 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   886
 516 -22 467 31 467 93 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   887
 467 111 471 118 471 127 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   888
 471 133 462 285 461 305 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   889
 460 319 459 343 457 344 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   890
 455 345 453 345 440 345 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   891
 343 345 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   892
 343 246 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   893
 343 117 285 -22 194 -22 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   894
 116 -22 84 62 75 85 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   895
 70 83 64 81 58 78 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   896
 51 79 46 84 46 90 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   897
 46 98 63 105 67 105 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   898
 66 108 63 115 63 118 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   899
 63 123 70 131 76 131 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   900
 83 131 90 119 90 114 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   901
 94 116 106 121 110 121 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   902
 115 121 121 115 121 110 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   903
 121 102 102 94 98 94 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   904
 127 13 169 0 193 0 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   905
 260 0 260 189 260 209 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   906
 260 476 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   907
 260 621 212 683 166 683 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   908
 118 683 86 634 86 587 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   909
 86 575 87 558 123 527 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   910
 194 462 194 419 194 394 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   911
 194 369 194 243 114 243 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   912
 57 243 56 320 56 321 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   913
 56 328 57 336 69 336 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   914
 80 336 81 328 81 321 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   915
 82 303 87 265 113 265 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   916
 154 265 162 316 162 383 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   917
 162 420 162 437 109 491 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   918
 80 520 56 546 56 585 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   919
 56 643 99 705 167 705 c 0xf7c0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   920
 228 705 278 658 308 602 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   921
 367 700 505 716 549 716 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   922
 562 716 565 716 572 703 c 2xfbc0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   923
624 439 m 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   924
 496 668 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   925
 491 677 490 678 487 678 c 0xfbc0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   926
 483 678 356 657 324 563 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   927
 343 507 343 460 343 447 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   928
 343 376 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   929
 490 376 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   930
 508 376 526 376 570 396 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   931
 580 400 630 424 630 428 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   932
 630 429 629 429 624 439 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   933
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   934
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   935
StartChar: weierstrass
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   936
Encoding: 8472 8472 30
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   937
Width: 636
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   938
Flags: W
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   939
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   940
HStem: -216 22<142 152> -11 22<379 397> -11 129<326 389> 388 22<475 493>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   941
VStem: 76 25<-135 -119> 83 46<185 213> 227 47<-80 -51> 298 25<71 75> 298 48<74 100> 557 61<259 291>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   942
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   943
169 122 m 1xd340
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   944
 182 104 217 61 230 43 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   945
 265 -1 274 -13 274 -51 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   946
 274 -130 209 -216 142 -216 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   947
 92 -216 76 -178 76 -135 c 0xdb40
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   948
 76 -89 100 15 124 78 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   949
 99 108 83 127 83 185 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   950
 83 316 174 453 246 453 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   951
 249 453 259 453 259 443 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   952
 259 433 252 432 245 431 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   953
 184 421 129 299 129 213 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   954
 129 199 129 168 152 144 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   955
 264 364 403 410 486 410 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   956
 574 410 618 337 618 259 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   957
 618 125 501 -11 389 -11 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   958
 332 -11 298 28 298 74 c 0xd740
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   959
 298 90 302 118 326 118 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   960
 344 118 346 102 346 100 c 0xb2c0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   961
 346 98 346 80 323 75 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   962
 324 22 365 11 388 11 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   963
 419 11 468 32 509 105 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   964
 532 147 557 240 557 291 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   965
 557 340 539 388 484 388 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   966
 419 388 276 353 169 122 c 1xd340
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   967
215 -39 m 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   968
 141 55 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   969
 127 8 101 -83 101 -135 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   970
 101 -155 101 -194 142 -194 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   971
 184 -194 227 -137 227 -80 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   972
 227 -65 225 -54 215 -39 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   973
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   974
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   975
StartChar: exclam
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   976
Encoding: 33 33 31
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   977
Width: 277
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   978
Flags: MW
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   979
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   980
HStem: 0 106<124.5 153.5> 187 21<133 144> 696 20<126 152>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   981
VStem: 86 106<38.5 67.5 665 681.5>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   982
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   983
192 665 m 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   984
 153 209 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   985
 152 192 149 187 139 187 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   986
 127 187 126 195 125 210 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   987
 86 665 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   988
 86 698 113 716 139 716 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   989
 165 716 192 698 192 665 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   990
192 53 m 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   991
 192 24 168 0 139 0 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   992
 110 0 86 24 86 53 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   993
 86 82 110 106 139 106 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   994
 168 106 192 82 192 53 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   995
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   996
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   997
StartChar: universal
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   998
Encoding: 8704 8704 32
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   999
Width: 555
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1000
Flags: HMW
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1001
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1002
HStem: -22 21<271 284.5> 411 40<142 142 142 414> 674 20
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1003
VStem: 0 556<673.5 679.5>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1004
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1005
551 656 m 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1006
 299 -2 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1007
 295 -13 291 -22 278 -22 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1008
 264 -22 261 -13 256 0 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1009
 5 657 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1010
 0 669 0 672 0 674 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1011
 0 685 10 694 20 694 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1012
 34 694 37 685 42 672 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1013
 126 451 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1014
 430 451 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1015
 515 674 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1016
 519 684 523 694 536 694 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1017
 548 694 556 685 556 674 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1018
 556 673 556 668 551 656 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1019
142 411 m 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1020
 278 55 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1021
 414 411 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1022
 142 411 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1023
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1024
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1025
StartChar: numbersign
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1026
Encoding: 35 35 33
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1027
Width: 833
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1028
Flags: MW
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1029
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1030
HStem: -194 21<181.5 195 410.5 424> 133 40<82 261 90 249 302 478 90 290 531 742 742 743> 327 40<89 90 90 301 89 342 354 530 583 742> 674 20<408 421.5 637 650.5>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1031
VStem: 56 720<143 163 337 357>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1032
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1033
519 133 m 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1034
 438 -170 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1035
 435 -181 432 -194 416 -194 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1036
 405 -194 396 -185 396 -174 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1037
 396 -170 399 -158 400 -156 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1038
 478 133 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1039
 290 133 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1040
 209 -170 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1041
 206 -181 203 -194 187 -194 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1042
 176 -194 167 -185 167 -174 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1043
 167 -170 170 -158 171 -156 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1044
 249 133 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1045
 89 133 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1046
 75 133 56 133 56 153 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1047
 56 173 75 173 90 173 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1048
 261 173 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1049
 301 327 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1050
 90 327 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1051
 75 327 56 327 56 347 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1052
 56 367 75 367 89 367 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1053
 313 367 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1054
 394 670 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1055
 397 681 400 694 416 694 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1056
 427 694 436 685 436 674 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1057
 436 670 433 658 432 656 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1058
 354 367 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1059
 542 367 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1060
 623 670 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1061
 626 681 629 694 645 694 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1062
 656 694 665 685 665 674 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1063
 665 670 662 658 661 656 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1064
 583 367 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1065
 743 367 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1066
 757 367 776 367 776 347 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1067
 776 327 757 327 742 327 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1068
 571 327 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1069
 531 173 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1070
 742 173 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1071
 757 173 776 173 776 153 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1072
 776 133 757 133 743 133 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1073
 519 133 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1074
302 173 m 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1075
 490 173 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1076
 530 327 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1077
 342 327 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1078
 302 173 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1079
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1080
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1081
StartChar: existential
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1082
Encoding: 8707 8707 34
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1083
Width: 555
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1084
Flags: W
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1085
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1086
HStem: 0 40<72.6953 459> 327 40<103 459> 654 40<72.6953 459>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1087
VStem: 459 40<39 661>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1088
CounterMasks: 1 00
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1089
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1090
499 661 m 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1091
 499 33 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1092
 499 4 495 0 466 0 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1093
 89 0 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1094
 75 0 56 0 56 20 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1095
 56 40 75 40 89 40 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1096
 459 40 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1097
 459 327 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1098
 103 327 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1099
 89 327 70 327 70 347 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1100
 70 367 89 367 103 367 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1101
 459 367 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1102
 459 654 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1103
 89 654 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1104
 75 654 56 654 56 674 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1105
 56 694 75 694 89 694 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1106
 466 694 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1107
 495 694 499 690 499 661 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1108
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1109
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1110
StartChar: percent
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1111
Encoding: 37 37 35
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1112
Width: 833
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1113
Flags: W
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1114
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1115
HStem: -56 22<637 673> 325 22<636.5 673.5> 347 22<194 230> 619 22<445 498.5> 728 22<193.5 219>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1116
VStem: 56 62<488.5 607.5> 308 25<495 555> 499 62<85.5 204.5> 751 25<92 198.5>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1117
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1118
685 712 m 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1119
 179 -41 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1120
 171 -52 169 -56 159 -56 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1121
 149 -56 139 -47 139 -36 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1122
 139 -34 139 -29 148 -16 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1123
 597 653 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1124
 596 654 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1125
 590 650 539 619 463 619 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1126
 427 619 377 624 312 661 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1127
 333 609 333 562 333 548 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1128
 333 436 276 347 203 347 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1129
 128 347 56 428 56 549 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1130
 56 666 127 750 203 750 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1131
 235 750 256 735 275 718 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1132
 330 666 392 641 462 641 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1133
 535 641 602 668 652 736 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1134
 658 743 663 750 673 750 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1135
 684 750 693 741 693 730 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1136
 693 724 691 721 685 712 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1137
204 369 m 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1138
 256 369 308 441 308 549 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1139
 308 654 257 728 204 728 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1140
 183 728 118 715 118 548 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1141
 118 382 184 369 204 369 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1142
647 -34 m 0xdf80
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1143
 699 -34 751 38 751 146 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1144
 751 251 700 325 647 325 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1145
 626 325 561 312 561 145 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1146
 561 -21 627 -34 647 -34 c 0xdf80
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1147
776 145 m 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1148
 776 33 719 -56 646 -56 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1149
 571 -56 499 25 499 146 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1150
 499 263 570 347 646 347 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1151
 717 347 776 260 776 145 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1152
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1153
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1154
StartChar: ampersand
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1155
Encoding: 38 38 36
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1156
Width: 777
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1157
Flags: MW
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1158
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1159
HStem: -22 31<189.5 245 557 606.5> 400 31<508 508 727 727> 694 22<283.5 331>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1160
VStem: 42 83<133 155> 163 63<562.5 608> 361 25<555 589> 693 28
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1161
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1162
696 121 m 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1163
 721 121 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1164
 719 35 656 -22 580 -22 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1165
 532 -22 473 -6 404 54 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1166
 367 21 308 -22 223 -22 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1167
 124 -22 42 41 42 128 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1168
 42 182 68 209 113 255 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1169
 143 287 184 330 204 352 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1170
 169 441 163 513 163 555 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1171
 163 661 237 716 299 716 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1172
 370 716 386 633 386 587 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1173
 386 521 318 445 264 385 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1174
 308 270 417 133 430 118 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1175
 473 171 518 239 573 336 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1176
 574 339 579 346 579 356 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1177
 579 381 554 400 508 400 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1178
 508 431 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1179
 535 429 619 428 630 428 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1180
 636 428 690 429 727 431 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1181
 727 400 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1182
 638 399 617 364 578 298 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1183
 532 219 492 151 446 98 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1184
 478 60 530 9 584 9 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1185
 629 9 693 42 696 121 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1186
256 409 m 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1187
 280 435 361 522 361 588 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1188
 361 590 361 694 301 694 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1189
 266 694 226 662 226 578 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1190
 226 547 229 489 256 409 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1191
213 329 m 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1192
 159 277 125 241 125 160 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1193
 125 106 148 9 231 9 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1194
 259 9 321 16 385 73 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1195
 348 110 312 162 293 190 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1196
 250 252 235 282 213 329 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1197
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1198
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1199
StartChar: uni220D
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1200
Encoding: 8717 8717 37
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1201
Width: 666
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1202
Flags: HMW
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1203
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1204
HStem: -40 40<116 276 276 279> 230 40<116 542> 500 40<116 275>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1205
VStem: 542 41<230 230 270 270>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1206
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1207
275 500 m 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1208
 116 500 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1209
 102 500 83 500 83 520 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1210
 83 540 102 540 116 540 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1211
 278 540 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1212
 441 540 583 416 583 250 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1213
 583 82 439 -40 279 -40 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1214
 116 -40 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1215
 102 -40 83 -40 83 -20 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1216
 83 0 102 0 116 0 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1217
 276 0 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1218
 412 0 530 94 542 230 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1219
 116 230 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1220
 102 230 83 230 83 250 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1221
 83 270 102 270 116 270 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1222
 542 270 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1223
 530 404 415 500 275 500 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1224
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1225
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1226
StartChar: parenleft
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1227
Encoding: 40 40 38
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1228
Width: 388
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1229
Flags: MW
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1230
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1231
HStem: -250 21<316 324> 730 20<316 324>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1232
VStem: 99 58<211 292>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1233
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1234
331 -240 m 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1235
 331 -247 327 -250 321 -250 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1236
 311 -250 225 -185 165 -62 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1237
 110 51 99 172 99 250 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1238
 99 334 111 445 162 555 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1239
 221 682 311 750 321 750 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1240
 327 750 331 747 331 740 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1241
 331 737 331 735 318 723 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1242
 195 598 157 424 157 250 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1243
 157 97 189 -92 314 -218 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1244
 331 -235 331 -237 331 -240 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1245
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1246
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1247
StartChar: parenright
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1248
Encoding: 41 41 39
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1249
Width: 388
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1250
Flags: MW
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1251
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1252
HStem: -250 21<64 72> 730 20<64 72>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1253
VStem: 231 58<208 289>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1254
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1255
289 250 m 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1256
 289 166 277 55 226 -55 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1257
 167 -182 77 -250 67 -250 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1258
 61 -250 57 -246 57 -240 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1259
 57 -237 57 -235 70 -223 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1260
 194 -97 231 79 231 250 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1261
 231 459 174 618 76 717 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1262
 57 735 57 737 57 740 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1263
 57 746 61 750 67 750 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1264
 77 750 163 685 223 562 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1265
 278 449 289 328 289 250 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1266
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1267
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1268
StartChar: asteriskmath
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1269
Encoding: 8727 8727 40
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1270
Width: 500
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1271
Flags: HMW
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1272
Validated: 33
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1273
HStem: 34 21<242 262.5> 445 20<242 262.5>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1274
VStem: 221 50
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1275
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1276
261 229 m 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1277
 275 71 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1278
 276 57 276 34 249 34 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1279
 235 34 221 46 224 61 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1280
 224 66 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1281
 238 230 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1282
 112 137 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1283
 101 129 96 128 92 128 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1284
 79 128 65 140 65 156 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1285
 65 172 77 178 86 182 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1286
 227 250 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1287
 86 317 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1288
 77 321 65 327 65 343 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1289
 65 359 79 371 92 371 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1290
 99 371 99 370 112 361 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1291
 238 269 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1292
 224 428 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1293
 224 439 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1294
 221 452 234 465 250 465 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1295
 275 465 276 442 275 429 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1296
 261 269 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1297
 387 362 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1298
 398 370 403 371 407 371 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1299
 420 371 434 359 434 343 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1300
 434 327 422 321 413 317 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1301
 271 249 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1302
 416 181 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1303
 430 174 434 164 434 156 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1304
 434 140 420 128 407 128 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1305
 400 128 382 141 370 150 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1306
 333 176 297 203 261 229 c 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1307
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1308
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1309
StartChar: plus
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1310
Encoding: 43 43 41
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1311
Width: 777
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1312
Flags: MW
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1313
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1314
HStem: -83 21<379 399> 230 40<89 369 409 688> 563 20<379 399>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1315
VStem: 369 40<-50 230 270 550>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1316
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1317
409 230 m 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1318
 409 -50 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1319
 409 -64 409 -83 389 -83 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1320
 369 -83 369 -64 369 -50 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1321
 369 230 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1322
 89 230 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1323
 75 230 56 230 56 250 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1324
 56 270 75 270 89 270 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1325
 369 270 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1326
 369 550 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1327
 369 564 369 583 389 583 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1328
 409 583 409 564 409 550 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1329
 409 270 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1330
 688 270 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1331
 702 270 721 270 721 250 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1332
 721 230 702 230 688 230 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1333
 409 230 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1334
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1335
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1336
StartChar: comma
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1337
Encoding: 44 44 42
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1338
Width: 277
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1339
Flags: MW
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1340
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1341
HStem: -193 21<109.5 118> 0 106<121.5 147>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1342
VStem: 181 22<-31 8>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1343
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1344
179 16 m 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1345
 177 14 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1346
 167 6 155 0 139 0 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1347
 103 0 86 27 86 53 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1348
 86 79 104 106 139 106 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1349
 179 106 203 65 203 1 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1350
 203 -114 124 -193 112 -193 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1351
 107 -193 102 -189 102 -182 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1352
 102 -178 103 -177 109 -171 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1353
 153 -124 181 -63 181 1 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1354
 181 15 180 16 179 16 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1355
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1356
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1357
StartChar: minus
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1358
Encoding: 8722 8722 43
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1359
Width: 777
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1360
Flags: HMW
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1361
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1362
HStem: 230 40<116 661>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1363
VStem: 83 611<240 260>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1364
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1365
661 230 m 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1366
 116 230 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1367
 102 230 83 230 83 250 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1368
 83 270 102 270 116 270 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1369
 661 270 l 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1370
 675 270 694 270 694 250 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1371
 694 230 675 230 661 230 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1372
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1373
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1374
StartChar: period
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1375
Encoding: 46 46 44
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1376
Width: 277
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1377
Flags: MW
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1378
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1379
HStem: 0 106<124.5 153.5>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1380
VStem: 86 106<38.5 67.5>
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1381
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1382
192 53 m 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1383
 192 24 168 0 139 0 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1384
 110 0 86 24 86 53 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1385
 86 82 110 106 139 106 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1386
 168 106 192 82 192 53 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1387
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1388
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1389
StartChar: slash
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1390
Encoding: 47 47 45
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1391
Width: 500
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1392
Flags: MW
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1393
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1394
HStem: -250 21<70.5 83> 730 20
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1395
VStem: 56 387
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1396
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1397
438 712 m 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1398
 97 -230 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1399
 94 -240 90 -250 76 -250 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1400
 65 -250 56 -241 56 -230 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1401
 56 -228 56 -225 61 -212 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1402
 402 730 l 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1403
 405 740 409 750 423 750 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1404
 434 750 443 741 443 730 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1405
 443 728 443 725 438 712 c 2
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1406
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1407
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1408
StartChar: zero
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1409
Encoding: 48 48 46
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1410
Width: 554
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1411
VWidth: 921
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1412
Flags: HMW
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1413
Validated: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1414
Fore
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1415
217.35 337.5 m 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1416
 217.35 354 223.125 368.25 234.675 380.25 c 128
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1417
 246.225 392.25 260.1 398.25 276.3 398.25 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1418
 293.1 398.25 307.5 392.25 319.5 380.25 c 128
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1419
 331.5 368.25 337.5 354 337.5 337.5 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1420
 337.5 320.7 331.575 306.45 319.725 294.75 c 128
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1421
 307.875 283.05 293.4 277.2 276.3 277.2 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1422
 259.5 277.2 245.475 282.9 234.225 294.3 c 128
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1423
 222.975 305.7 217.35 320.1 217.35 337.5 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1424
277.2 612 m 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1425
 234.9 612 203.325 589.2 182.475 543.6 c 128
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1426
 161.625 498 151.2 428.55 151.2 335.25 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1427
 151.2 242.25 161.625 172.95 182.475 127.35 c 128
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1428
 203.325 81.75 234.9 58.9502 277.2 58.9502 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1429
 319.8 58.9502 351.525 81.75 372.375 127.35 c 128
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1430
 393.225 172.95 403.65 242.25 403.65 335.25 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1431
 403.65 428.55 393.225 498 372.375 543.6 c 128
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1432
 351.525 589.2 319.8 612 277.2 612 c 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1433
277.2 684 m 256
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1434
 348.9 684 403.125 654.6 439.875 595.8 c 128