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