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