lib/fonts/IsabelleMono.sfd
author wenzelm
Fri, 16 Apr 2010 10:52:10 +0200
changeset 36162 0bd034a80a9a
parent 29085 29de5c277f2a
permissions -rw-r--r--
added ML antiquotation @{make_string}, which produces proper pretty printed version in Poly/ML 5.3.0 or later;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
29073
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
     1
SplineFontDB: 2.0
29078
006334dd31a0 renamed to IsabelleMono;
wenzelm
parents: 29074
diff changeset
     2
FontName: IsabelleMono
006334dd31a0 renamed to IsabelleMono;
wenzelm
parents: 29074
diff changeset
     3
FullName: IsabelleMono
006334dd31a0 renamed to IsabelleMono;
wenzelm
parents: 29074
diff changeset
     4
FamilyName: IsabelleMono
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
     5
Weight: Book
29078
006334dd31a0 renamed to IsabelleMono;
wenzelm
parents: 29074
diff changeset
     6
Copyright: 
006334dd31a0 renamed to IsabelleMono;
wenzelm
parents: 29074
diff changeset
     7
Version: IsabelleMono
29073
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
     8
ItalicAngle: 0
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
     9
UnderlinePosition: -283
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    10
UnderlineWidth: 141
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    11
Ascent: 1556
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    12
Descent: 492
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    13
Order2: 1
29080
2671cb2e55ac added glyphs for \<A> (cal), \<a> (rm), \<AA> (\frak), \<aa> (frak);
wenzelm
parents: 29078
diff changeset
    14
NeedsXUIDChange: 1
29078
006334dd31a0 renamed to IsabelleMono;
wenzelm
parents: 29074
diff changeset
    15
XUID: [1021 906 1711068302 1934665]
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    16
FSType: 4
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    17
OS2Version: 1
29073
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    18
OS2_WeightWidthSlopeOnly: 0
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    19
OS2_UseTypoMetrics: 1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    20
CreationTime: 1050361371
29085
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
    21
ModificationTime: 1220730733
29073
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    22
PfmFamily: 17
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    23
TTFWeight: 400
29073
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    24
TTFWidth: 5
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    25
LineGap: 0
29073
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    26
VLineGap: 0
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    27
Panose: 2 11 6 9 3 8 4 2 2 4
29073
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    28
OS2TypoAscent: 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    29
OS2TypoAOffset: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    30
OS2TypoDescent: 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    31
OS2TypoDOffset: 1
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    32
OS2TypoLinegap: 410
29073
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    33
OS2WinAscent: 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    34
OS2WinAOffset: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    35
OS2WinDescent: 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    36
OS2WinDOffset: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    37
HheadAscent: 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    38
HheadAOffset: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    39
HheadDescent: 0
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    40
HheadDOffset: 1
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    41
OS2SubXSize: 1351
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    42
OS2SubYSize: 1228
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    43
OS2SubXOff: 0
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    44
OS2SubYOff: -446
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    45
OS2SupXSize: 1351
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    46
OS2SupYSize: 1228
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    47
OS2SupXOff: 0
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    48
OS2SupYOff: 595
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    49
OS2StrikeYSize: 141
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    50
OS2StrikeYPos: 614
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    51
OS2FamilyClass: 2050
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    52
OS2Vendor: 'Bits'
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    53
OS2CodePages: 00000001.00000000
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    54
OS2UnicodeRanges: 800000af.1000204a.00000000.00000000
29073
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
    55
DEI: 0
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    56
TtfTable: prep 1819
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    57
\H79^'sa'0"[O+/'`aO"!s',:J,f]Q'EJ+4!s'&8rW!$$&c`OE!s&u6rW!$$&-2\0!s&o4RK*Ej
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    58
%KQJ.!s&k:lUM+E,lnGTI/j?M$ihRR!s&c01&qCW$36@l!s&].rW!$$#QP>7!s&W,rW!$$"ooqL
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    59
!s&Q*rW!$$"98o3!s&K(,le#J!W`3"!s&Ef=oJO&rWE+I"8r-#qu-]o1'@?a"8I9Hp\'OLp\k9h
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    60
^]aB(=U"MX"876Jp%0R7oiVCi5Qp^+"7u(:"nVQmnh1+8rWDZh"7IuImM#cjQ36L>7g88Y"73Pt
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    61
d6R^7lUM'Bl!st_Q36A^"6f^dkN3]ekPbSG)[#4$"6=5"j8K/?]*%$M)$T!q"5k%!hj+B$rWD!U
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    62
"5MWG"l0(ZgD'hEQ35gm'a<:i"5&S@"kXOlf6mbP3Wmol$O,'A"4[;Pe'\R,e,BHt$3S]T"47#L
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    63
c\`;<cQ!&4('Dh\"3d&5bDRYMbPhUdrWC8j"3CHDa8Q1\rWC-.%0a]L"2k*?_YsYRrWBrq$O+<[
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    64
"2>6H^:h,^^A\5J]Nk]S]*#`s"MD>m"h\+C]KcV3,m1aX"1a^"\;roZ\,HK<O$NrXq?+-o%0a-<
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    65
"1)M?Z=F'B%KipJ"0_\+Y5U]b"0MP)XSr=&&d,05"0&4/"fX6ZW"&p-V@a!0-j-=Y"/VeF"f6VL
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    66
Ub)\DrWAno"/5\rTV!)*TO\.sSe)'t)$?HA".]c$SGiV[RLKFirWASu".>N/"e#>lQnAK-O$Nr9
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    67
Q33G<]*4N""-o*V"dQ\%Q%0"%O<k'p>m$<V"I&feP5YQGO<k'm]*"-@"-8?d"ckqONf=DMNYDST
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    68
$Nl?G,mB6<",i$K"cFZ/M@frIrW@uU",HjXL4p3CLAh:/&Hd^c",$RTJe:<QJl;c&rW@[q"+PcJ
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    69
"b6LRIXM<H*Wpfh"+(L[HN""jrW@?C"*J\o"a(=XFgqGP5hZ?_$j1Ue"EP1XF$KkKrW@0>"*"5A
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    70
Df/JWDjCKCD(#R*;Zgkb")Rr=CGH!,rW?ji").N5B=e7XrW?a2"(_B5@q$J_A,ZR>!"]<C*WojM
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    71
"(;*1?iC.6=pkL?%Kg!I"'inL>?VC<>8.0C$NjQ2"'?6>=8i;&rW?.>)$O"q"'#7%;uQksrW?#G
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    72
"&St!:D<n+rW>jq/HnlJ"&-</9.0m78JhV'2ZlW=&d:iD"%Yit"\AUp7mdmm7q;]k72Q1t])tJ=
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    73
"%5Kh"[k9O6UD@g6P9Jg\,no\#m<R\%g>93"%'L!!'ghn5sPn`5n=&`\,jB1#m<LX$jAm+"$j?s
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    74
J3XDD57@i%57@WY\,ei[A->*q"$HZ:"[2\a4T5FE-j)O0"$$r["Z^)q3&)<T3(j?4rW>&1'EpDo
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    75
"#W^R1b]gO1eRp,0H(*NrW=nf63T.D"#2AA"Ygnt0H($H/JJ@A(]uAs('Q>&""c&;"YCDj/[tk4
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    76
5R@QE&.o's'*Beq!^K#:"=krJ"Y9QS.L?jo.O>0G!]gK6rW=SJ""4'M-4^2)(.&0N70=eG"!ddI
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    77
+qG1f,5qZf+>!a?I01TD"!:/<*YC^B*rZ6^rW=,Z)$M#Z!uh4O"WJ<])ZBgVrW=#:!uD_>"W'W1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    78
()8D)(.&*<'G(E_/HZ[u!ttYG"VVRP&eRG6')htF!A+He63@c0%g<LV!t_sD!'ghn%h9!O%hAaQ
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    79
\,jB1#m:_I$3^nJ!tMgAJ3XDD%1EOH%131H\,ek%":PS=%(H<<5W8fRrW<K6('P'E!so_F#S7(C
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    80
rW<?*/Hl@X!sKA@!s1Le"8W*$!A+HV3WfB_&-W(d!rrl7!Or/@KoH*`.k<,#.k<,#.k<,#.k<,#
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    81
.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    82
.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    83
.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    84
.k<,#.k:TM.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    85
.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    86
.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#.k<,#
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    87
.k<,#.k<,#.k<,#.k<,#.k;V?
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    88
EndTtf
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    89
TtfTable: fpgm 140
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    90
[KZm<!s/K'/0GM.![UEKYWu&f+NR\//M++-,tVXO5Z(W+aB9Z</0GK/+KtiBYRPk#\GuS*=9KQH
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    91
=g/&LYQH0WYQQ6si?5?):p:CS+LqIO:fmi>"^/&5*3]Mk#iR?d92J_5\,dC76s1Zb/?f1%7:8M8
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    92
/5&oDYQ?,T![U9'=Wnq?/4DrY
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    93
EndTtf
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    94
TtfTable: cvt  560
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    95
!4W$P!4W$P!3-'^!4W#@!!!#/!/CW*!!3-%!!3-%!!3/1!5ef[!!3/D!4W$=!QtM#!P/9S!2]bo
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    96
!6Y@p!:g-t"31F$!.t9c!!!"$"<dcg!07,M!!3-%!076F!-JCV!7Lqi!8@Kr"6T\F"1eKU!Rh#l
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    97
!T*me!/U[W!!3-%!!3-%"24bl!5eoQ!.+g^"'>RG!Gqh4!NlD&!.+^U!H.sf!dapW!`B#Z!6kYo
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    98
!!!#D!/CQ0!0[DY!,hk^!6YAP!.t<7!8RX^!/gjL!13iP!*TB0!4i0L"<ddE!"Ju1!!3-%!S%2D
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
    99
!.P'M!^-Ts!/gir!07,K!1Eq@!7_'j"98H0!<)uW"k<Z)!2KV%!1X#h!+Gqu"k<dD!/CW*"k<e,
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   100
"n2Mf!!!!>#.OjO#9s8u!4W$P!2]e0!AOXN!7LrU!.+]F"'bqJ"5<j1"="%n"6ffH!WW=1!,;M[
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   101
"k<ek!07@0!07=r!I4fU"CM@?"FC+K!.+ck"CM81!9j\%#@[f1!.+bj!6"r.!.P&s!!!#+!`B1s
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   102
"\o3J!+l5$!1X%$!1X%M!+l5$!07<q!6kWB!.t96!r`3k"@`JX!07,,"AAf_!29Gn!%.bb!!!";
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   103
"#U'n!,hja"cW\F"cW\F!3-%!!%eA6"-s"8!;6DB!ic8W!^-OR!bMIk!073T!6kL^"%3,J!+l3O
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   104
"muAE!ON%F!!!7P!-8=o!!!]5
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   105
EndTtf
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   106
TtfTable: maxp 32
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   107
!!*'"!=]$'!!`Kn!!E9'!"],q!!`K("]kpJ!!<3%
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   108
EndTtf
29078
006334dd31a0 renamed to IsabelleMono;
wenzelm
parents: 29074
diff changeset
   109
LangName: 1033 "" "" "" "" "" "Release 1.10" "" "Bitstream Vera is a trademark of Bitstream, Inc." "Bitstream Inc." "" "" "http://www.bitstream.com" "" "Copyright (c) 2003 by Bitstream, Inc.+AA0ACgAA-All Rights Reserved.+AA0ACgAA-Bitstream Vera is a trademark of Bitstream, Inc.+AA0ACgANAAoA-Permission is hereby granted, free of charge, to any person obtaining a copy of the fonts accompanying this license (+ACIA-Fonts+ACIA) and associated documentation files (the +ACIA-Font Software+ACIA), to reproduce and distribute the Font Software, including without limitation the rights to use, copy, merge, publish, distribute, and/or sell copies of the Font Software, and to permit persons to whom the Font Software is furnished to do so, subject to the following conditions:+AA0ACgANAAoA-The above copyright and trademark notices and this permission notice shall be included in all copies of one or more of the Font Software typefaces.+AA0ACgANAAoA-The Font Software may be modified, altered, or added to, and in particular the designs of glyphs or characters in the Fonts may be modified and additional glyphs or characters may be added to the Fonts, only if the fonts are renamed to names not containing either the words +ACIA-Bitstream+ACIA or the word +ACIA-Vera+ACIA.+AA0ACgANAAoA-This License becomes null and void to the extent applicable to Fonts or Font Software that has been modified and is distributed under the +ACIA-Bitstream Vera+ACIA names.+AA0ACgANAAoA-The Font Software may be sold as part of a larger software package but no copy of one or more of the Font Software typefaces may be sold by itself.+AA0ACgANAAoA-THE FONT SOFTWARE IS PROVIDED +ACIA-AS IS+ACIA, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO ANY WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT OF COPYRIGHT, PATENT, TRADEMARK, OR OTHER RIGHT. IN NO EVENT SHALL BITSTREAM OR THE GNOME FOUNDATION BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, INCLUDING ANY GENERAL, SPECIAL, INDIRECT, INCIDENTAL, OR CONSEQUENTIAL DAMAGES, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF THE USE OR INABILITY TO USE THE FONT SOFTWARE OR FROM OTHER DEALINGS IN THE FONT SOFTWARE.+AA0ACgANAAoA-Except as contained in this notice, the names of Gnome, the Gnome Foundation, and Bitstream Inc., shall not be used in advertising or otherwise to promote the sale, use or other dealings in this Font Software without prior written authorization from the Gnome Foundation or Bitstream Inc., respectively. For further information, contact: fonts at gnome dot org." 
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   110
GaspTable: 2 8 2 65535 3
29073
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   111
Encoding: UnicodeFull
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   112
UnicodeInterp: none
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   113
NameList: Adobe Glyph List
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   114
DisplaySize: -48
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   115
AntiAlias: 1
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   116
FitToEm: 1
29085
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   117
WinInfo: 0 16 14
29080
2671cb2e55ac added glyphs for \<A> (cal), \<a> (rm), \<AA> (\frak), \<aa> (frak);
wenzelm
parents: 29078
diff changeset
   118
BeginChars: 1114112 652
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   119
StartChar: u10000
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   120
Encoding: 65536 65536 0
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   121
Width: 1233
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   122
Flags: W
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   123
TtfInstrs: 31
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   124
]Dr'8'EA+5"p#FH!=/j]!X&KV`74-.!"dZHeEejh
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   125
EndTtf
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   126
Fore
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   127
104 -362 m 1,0,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   128
 104 1444 l 1,1,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   129
 1128 1444 l 1,2,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   130
 1128 -362 l 1,3,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   131
 104 -362 l 1,0,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   132
219 -248 m 1,4,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   133
 1014 -248 l 1,5,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   134
 1014 1329 l 1,6,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   135
 219 1329 l 1,7,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   136
 219 -248 l 1,4,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   137
EndSplineSet
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   138
EndChar
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   139
StartChar: u10001
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   140
Encoding: 65537 65537 1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   141
Width: 0
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   142
Flags: W
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   143
EndChar
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   144
StartChar: u10002
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   145
Encoding: 65538 65538 2
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   146
Width: 1233
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   147
Flags: W
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   148
EndChar
29073
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   149
StartChar: space
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   150
Encoding: 32 32 3
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   151
Width: 1233
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   152
Flags: W
29073
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   153
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   154
StartChar: exclam
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   155
Encoding: 33 33 4
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   156
Width: 614
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   157
VWidth: 2220
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   158
Flags: W
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   159
HStem: 0 235.32<276.39 340.77> 415.14 46.62<295.26 319.68> 1545.12 44.4<279.72 337.44>
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   160
VStem: 190.92 235.32<85.47 149.85 1476.3 1512.93>
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   161
Fore
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   162
426.24 1476.3 m 2,0,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   163
 339.66 463.98 l 2,1,2
29085
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   164
 337.987 435.531 337.987 435.531 331.567 425.335 c 128,-1,3
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   165
 325.148 415.14 325.148 415.14 308.58 415.14 c 0,4,5
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   166
 290.194 415.14 290.194 415.14 284.807 426.273 c 128,-1,6
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   167
 279.419 437.406 279.419 437.406 277.5 466.2 c 2,7,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   168
 190.92 1476.3 l 2,8,9
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   169
 190.92 1528.31 190.92 1528.31 226.404 1558.92 c 128,-1,10
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   170
 261.888 1589.52 261.888 1589.52 308.58 1589.52 c 128,-1,11
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   171
 355.273 1589.52 355.273 1589.52 390.756 1558.92 c 128,-1,12
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   172
 426.24 1528.31 426.24 1528.31 426.24 1476.3 c 2,0,-1
29085
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   173
426.24 117.66 m 128,-1,14
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   174
 426.24 69.3752 426.24 69.3752 391.553 34.6876 c 128,-1,15
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   175
 356.865 0 356.865 0 308.58 0 c 128,-1,16
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   176
 260.295 0 260.295 0 225.608 34.6876 c 128,-1,17
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   177
 190.92 69.3752 190.92 69.3752 190.92 117.66 c 128,-1,18
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   178
 190.92 165.945 190.92 165.945 225.608 200.633 c 128,-1,19
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   179
 260.295 235.32 260.295 235.32 308.58 235.32 c 128,-1,20
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   180
 356.865 235.32 356.865 235.32 391.553 200.633 c 128,-1,13
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   181
 426.24 165.945 426.24 165.945 426.24 117.66 c 128,-1,14
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   182
EndSplineSet
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   183
EndChar
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   184
StartChar: quotedbl
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   185
Encoding: 34 34 5
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   186
Width: 1233
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   187
Flags: W
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   188
TtfInstrs: 29
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   189
5RmquM$*g7#QOu/"p>&7&Cg(%lnJJOoK;Iq0E;(Q
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   190
EndTtf
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   191
Fore
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   192
895 1493 m 1,0,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   193
 895 938 l 1,1,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   194
 721 938 l 1,2,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   195
 721 1493 l 1,3,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   196
 895 1493 l 1,0,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   197
512 1493 m 1,4,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   198
 512 938 l 1,5,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   199
 338 938 l 1,6,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   200
 338 1493 l 1,7,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   201
 512 1493 l 1,4,-1
29073
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   202
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   203
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   204
StartChar: numbersign
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   205
Encoding: 35 35 6
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   206
Width: 1849
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   207
VWidth: 2220
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   208
Flags: W
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   209
HStem: -430.68 46.62<402.93 432.9 911.31 941.28> 295.26 88.8<182.04 579.42 199.8 552.78 670.44 1061.16 199.8 643.8 1178.82 1647.24 1647.24 1649.46> 725.94 88.8<197.58 199.8 199.8 668.22 197.58 759.24 785.88 1176.6 1294.26 1647.24> 1496.28 44.4<905.76 935.73 1414.14 1444.11>
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   210
VStem: 124.32 1598.4<317.46 361.86 748.14 792.54>
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   211
Fore
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   212
1152.18 295.26 m 1,0,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   213
 972.36 -377.4 l 2,1,2
29085
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   214
 968.668 -390.94 968.668 -390.94 966.597 -396.758 c 128,-1,3
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   215
 964.527 -402.575 964.527 -402.575 959.08 -412.467 c 128,-1,4
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   216
 953.633 -422.359 953.633 -422.359 944.882 -426.519 c 128,-1,5
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   217
 936.132 -430.68 936.132 -430.68 923.52 -430.68 c 0,6,7
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   218
 905.205 -430.68 905.205 -430.68 892.162 -417.637 c 128,-1,8
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   219
 879.12 -404.595 879.12 -404.595 879.12 -386.28 c 0,9,10
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   220
 879.12 -380.096 879.12 -380.096 882.624 -365.081 c 128,-1,11
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   221
 886.127 -350.066 886.127 -350.066 888 -346.32 c 2,12,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   222
 1061.16 295.26 l 1,13,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   223
 643.8 295.26 l 1,14,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   224
 463.98 -377.4 l 2,15,16
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   225
 460.288 -390.94 460.288 -390.94 458.217 -396.758 c 128,-1,17
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   226
 456.147 -402.575 456.147 -402.575 450.7 -412.467 c 128,-1,18
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   227
 445.253 -422.359 445.253 -422.359 436.502 -426.519 c 128,-1,19
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   228
 427.752 -430.68 427.752 -430.68 415.14 -430.68 c 0,20,21
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   229
 396.825 -430.68 396.825 -430.68 383.782 -417.637 c 128,-1,22
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   230
 370.74 -404.595 370.74 -404.595 370.74 -386.28 c 0,23,24
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   231
 370.74 -380.096 370.74 -380.096 374.244 -365.081 c 128,-1,25
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   232
 377.747 -350.066 377.747 -350.066 379.62 -346.32 c 2,26,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   233
 552.78 295.26 l 1,27,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   234
 197.58 295.26 l 2,28,29
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   235
 181.346 295.26 181.346 295.26 172.258 296.109 c 128,-1,30
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   236
 163.17 296.958 163.17 296.958 150.058 300.654 c 128,-1,31
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   237
 136.946 304.351 136.946 304.351 130.633 314.147 c 128,-1,32
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   238
 124.32 323.942 124.32 323.942 124.32 339.66 c 0,33,34
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   239
 124.32 352.411 124.32 352.411 129.409 361.278 c 128,-1,35
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   240
 134.497 370.145 134.497 370.145 140.864 374.518 c 128,-1,36
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   241
 147.231 378.891 147.231 378.891 159.281 381.169 c 128,-1,37
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   242
 171.331 383.447 171.331 383.447 178.728 383.753 c 128,-1,38
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   243
 186.125 384.06 186.125 384.06 199.8 384.06 c 2,39,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   244
 579.42 384.06 l 1,40,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   245
 668.22 725.94 l 1,41,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   246
 199.8 725.94 l 2,42,43
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   247
 186.125 725.94 186.125 725.94 178.728 726.247 c 128,-1,44
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   248
 171.33 726.553 171.33 726.553 159.281 728.831 c 128,-1,45
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   249
 147.231 731.109 147.231 731.109 140.864 735.482 c 128,-1,46
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   250
 134.497 739.855 134.497 739.855 129.408 748.722 c 128,-1,47
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   251
 124.32 757.589 124.32 757.589 124.32 770.34 c 0,48,49
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   252
 124.32 786.058 124.32 786.058 130.633 795.853 c 128,-1,50
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   253
 136.946 805.649 136.946 805.649 150.058 809.346 c 128,-1,51
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   254
 163.17 813.042 163.17 813.042 172.258 813.891 c 128,-1,52
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   255
 181.346 814.74 181.346 814.74 197.58 814.74 c 2,53,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   256
 694.86 814.74 l 1,54,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   257
 874.68 1487.4 l 2,55,56
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   258
 878.372 1500.94 878.372 1500.94 880.443 1506.76 c 128,-1,57
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   259
 882.513 1512.58 882.513 1512.58 887.96 1522.47 c 128,-1,58
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   260
 893.407 1532.36 893.407 1532.36 902.157 1536.52 c 128,-1,59
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   261
 910.908 1540.68 910.908 1540.68 923.52 1540.68 c 0,60,61
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   262
 941.835 1540.68 941.835 1540.68 954.878 1527.64 c 128,-1,62
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   263
 967.92 1514.6 967.92 1514.6 967.92 1496.28 c 0,63,64
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   264
 967.92 1490.1 967.92 1490.1 964.416 1475.08 c 128,-1,65
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   265
 960.913 1460.07 960.913 1460.07 959.04 1456.32 c 2,66,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   266
 785.88 814.74 l 1,67,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   267
 1203.24 814.74 l 1,68,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   268
 1383.06 1487.4 l 2,69,70
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   269
 1386.75 1500.94 1386.75 1500.94 1388.82 1506.76 c 128,-1,71
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   270
 1390.89 1512.58 1390.89 1512.58 1396.34 1522.47 c 128,-1,72
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   271
 1401.79 1532.36 1401.79 1532.36 1410.54 1536.52 c 128,-1,73
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   272
 1419.29 1540.68 1419.29 1540.68 1431.9 1540.68 c 0,74,75
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   273
 1450.22 1540.68 1450.22 1540.68 1463.26 1527.64 c 128,-1,76
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   274
 1476.3 1514.6 1476.3 1514.6 1476.3 1496.28 c 0,77,78
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   275
 1476.3 1490.1 1476.3 1490.1 1472.8 1475.08 c 128,-1,79
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   276
 1469.29 1460.07 1469.29 1460.07 1467.42 1456.32 c 2,80,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   277
 1294.26 814.74 l 1,81,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   278
 1649.46 814.74 l 2,82,83
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   279
 1665.69 814.74 1665.69 814.74 1674.78 813.891 c 128,-1,84
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   280
 1683.87 813.042 1683.87 813.042 1696.98 809.346 c 128,-1,85
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   281
 1710.09 805.649 1710.09 805.649 1716.41 795.853 c 128,-1,86
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   282
 1722.72 786.058 1722.72 786.058 1722.72 770.34 c 0,87,88
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   283
 1722.72 757.589 1722.72 757.589 1717.63 748.722 c 128,-1,89
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   284
 1712.54 739.855 1712.54 739.855 1706.18 735.482 c 128,-1,90
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   285
 1699.81 731.109 1699.81 731.109 1687.76 728.831 c 128,-1,91
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   286
 1675.71 726.553 1675.71 726.553 1668.31 726.247 c 128,-1,92
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   287
 1660.91 725.94 1660.91 725.94 1647.24 725.94 c 2,93,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   288
 1267.62 725.94 l 1,94,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   289
 1178.82 384.06 l 1,95,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   290
 1647.24 384.06 l 2,96,97
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   291
 1660.92 384.06 1660.92 384.06 1668.31 383.753 c 128,-1,98
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   292
 1675.71 383.447 1675.71 383.447 1687.76 381.169 c 128,-1,99
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   293
 1699.81 378.891 1699.81 378.891 1706.18 374.518 c 128,-1,100
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   294
 1712.54 370.145 1712.54 370.145 1717.63 361.278 c 128,-1,101
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   295
 1722.72 352.411 1722.72 352.411 1722.72 339.66 c 0,102,103
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   296
 1722.72 323.942 1722.72 323.942 1716.41 314.147 c 128,-1,104
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   297
 1710.09 304.351 1710.09 304.351 1696.98 300.654 c 128,-1,105
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   298
 1683.87 296.958 1683.87 296.958 1674.78 296.109 c 128,-1,106
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   299
 1665.69 295.26 1665.69 295.26 1649.46 295.26 c 2,107,-1
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   300
 1152.18 295.26 l 1,0,-1
29085
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   301
670.44 384.06 m 1,108,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   302
 1087.8 384.06 l 1,109,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   303
 1176.6 725.94 l 1,110,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   304
 759.24 725.94 l 1,111,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   305
 670.44 384.06 l 1,108,-1
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   306
EndSplineSet
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   307
EndChar
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   308
StartChar: dollar
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   309
Encoding: 36 36 7
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   310
Width: 1110
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   311
VWidth: 2220
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   312
Flags: W
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   313
HStem: -124.32 46.62<519.48 588.3 519.48 519.48> -22.2 68.82<588.3 588.3> 304.14 204.24<222 254.19 219.78 256.41> 1063.38 204.24<858.03 884.67> 1494.06 66.6 1620.6 44.4<519.48 588.3 588.3 588.3>
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   314
VStem: 124.32 113.22<1183.26 1239.87> 124.32 204.24<376.29 437.34 376.29 449.55> 519.48 68.82<-124.32 -24.42 -24.42 -24.42 46.62 690.42 912.42 1494.06 1565.1 1665> 779.22 204.24<1131.09 1196.58> 870.24 113.22<318.57 392.94>
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   315
Fore
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   316
588.3 690.42 m 1,0,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   317
 588.3 46.6201 l 1,1,2
29085
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   318
 673.002 57.342 673.002 57.342 738.42 105.867 c 128,-1,3
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   319
 803.839 154.392 803.839 154.392 837.04 222.693 c 128,-1,4
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   320
 870.24 290.995 870.24 290.995 870.24 366.3 c 0,5,6
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   321
 870.24 381.638 870.24 381.638 868.772 398.364 c 128,-1,7
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   322
 867.304 415.09 867.304 415.09 860.776 443.902 c 128,-1,8
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   323
 854.249 472.715 854.249 472.715 843.323 499.008 c 128,-1,9
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   324
 832.398 525.302 832.398 525.302 810.94 556.08 c 128,-1,10
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   325
 789.482 586.859 789.482 586.859 760.866 611.458 c 128,-1,11
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   326
 732.25 636.058 732.25 636.058 687.629 657.54 c 128,-1,12
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   327
 643.008 679.022 643.008 679.022 588.3 690.42 c 1,0,-1
29085
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   328
519.48 708.18 m 1,13,14
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   329
 472.923 720.047 472.923 720.047 454.189 725.16 c 128,-1,15
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   330
 435.455 730.273 435.455 730.273 400.263 742.242 c 128,-1,16
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   331
 365.071 754.21 365.071 754.21 344.858 765.76 c 128,-1,17
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   332
 324.645 777.309 324.645 777.309 297.859 796.694 c 128,-1,18
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   333
 271.072 816.079 271.072 816.079 246.42 841.38 c 0,19,20
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   334
 228.525 858.281 228.525 858.281 209.999 883.296 c 128,-1,21
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   335
 191.473 908.31 191.473 908.31 170.87 945.776 c 128,-1,22
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   336
 150.268 983.242 150.268 983.242 137.294 1034.12 c 128,-1,23
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   337
 124.32 1084.99 124.32 1084.99 124.32 1138.86 c 0,24,25
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   338
 124.32 1214.92 124.32 1214.92 151.868 1287.31 c 128,-1,26
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   339
 179.417 1359.7 179.417 1359.7 229.035 1418.21 c 128,-1,27
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   340
 278.654 1476.72 278.654 1476.72 354.235 1515.76 c 128,-1,28
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   341
 429.816 1554.8 429.816 1554.8 519.48 1562.88 c 1,29,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   342
 519.48 1665 l 1,30,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   343
 588.3 1665 l 1,31,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   344
 588.3 1565.1 l 1,32,33
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   345
 771.538 1555.28 771.538 1555.28 877.499 1447.15 c 128,-1,34
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   346
 983.46 1339.02 983.46 1339.02 983.46 1174.38 c 0,35,36
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   347
 983.46 1143.85 983.46 1143.85 973.12 1121.27 c 128,-1,37
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   348
 962.78 1098.7 962.78 1098.7 949.791 1088.1 c 128,-1,38
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   349
 936.801 1077.51 936.801 1077.51 919.805 1071.33 c 128,-1,39
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   350
 902.808 1065.16 902.808 1065.16 894.877 1064.27 c 128,-1,40
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   351
 886.945 1063.38 886.945 1063.38 881.34 1063.38 c 0,41,42
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   352
 842.189 1063.38 842.189 1063.38 810.705 1090.43 c 128,-1,43
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   353
 779.22 1117.48 779.22 1117.48 779.22 1165.5 c 0,44,45
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   354
 779.22 1211.35 779.22 1211.35 808.236 1239.48 c 128,-1,46
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   355
 837.252 1267.62 837.252 1267.62 881.34 1267.62 c 0,47,48
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   356
 899.104 1267.62 899.104 1267.62 916.86 1263.18 c 1,49,50
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   357
 890.44 1361.82 890.44 1361.82 807.093 1424.75 c 128,-1,51
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   358
 723.746 1487.69 723.746 1487.69 588.3 1494.06 c 1,52,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   359
 588.3 894.66 l 1,53,54
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   360
 639.915 881.756 639.915 881.756 665.933 873.894 c 128,-1,55
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   361
 691.95 866.031 691.95 866.031 730.447 849.867 c 128,-1,56
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   362
 768.945 833.702 768.945 833.702 800.243 809.653 c 128,-1,57
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   363
 831.541 785.603 831.541 785.603 863.58 750.36 c 0,58,59
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   364
 876.11 737.83 876.11 737.83 891.58 716.537 c 128,-1,60
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   365
 907.049 695.245 907.049 695.245 930.173 654.937 c 128,-1,61
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   366
 953.296 614.629 953.296 614.629 968.378 555.726 c 128,-1,62
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   367
 983.46 496.824 983.46 496.824 983.46 432.9 c 0,63,64
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   368
 983.46 318.895 983.46 318.895 933.957 218.629 c 128,-1,65
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   369
 884.455 118.362 884.455 118.362 793.203 52.9518 c 128,-1,66
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   370
 701.951 -12.4585 701.951 -12.4585 588.3 -22.2002 c 1,67,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   371
 588.3 -124.32 l 1,68,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   372
 519.48 -124.32 l 1,69,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   373
 519.48 -24.4199 l 1,70,71
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   374
 438.779 -19.2551 438.779 -19.2551 372.121 7.13136 c 128,-1,72
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   375
 305.463 33.5178 305.463 33.5178 260.207 73.9785 c 128,-1,73
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   376
 214.95 114.439 214.95 114.439 183.794 167.291 c 128,-1,74
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   377
 152.639 220.143 152.639 220.143 138.479 277.295 c 128,-1,75
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   378
 124.32 334.447 124.32 334.447 124.32 395.16 c 0,76,77
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   379
 124.32 425.782 124.32 425.782 133.982 448.505 c 128,-1,78
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   380
 143.643 471.228 143.643 471.228 156.111 482.208 c 128,-1,79
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   381
 168.578 493.188 168.578 493.188 185.059 499.654 c 128,-1,80
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   382
 201.541 506.119 201.541 506.119 210.385 507.25 c 128,-1,81
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   383
 219.23 508.38 219.23 508.38 226.44 508.38 c 0,82,83
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   384
 269.262 508.38 269.262 508.38 298.911 480.058 c 128,-1,84
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   385
 328.56 451.737 328.56 451.737 328.56 406.26 c 0,85,86
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   386
 328.56 361.305 328.56 361.305 299.977 332.722 c 128,-1,87
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   387
 271.395 304.14 271.395 304.14 226.44 304.14 c 0,88,89
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   388
 208.684 304.14 208.684 304.14 190.92 308.58 c 1,90,91
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   389
 214.025 198.387 214.025 198.387 297.011 126.466 c 128,-1,92
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   390
 379.996 54.5451 379.996 54.5451 519.48 46.6201 c 1,93,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   391
 519.48 708.18 l 1,13,14
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   392
519.48 912.42 m 1,94,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   393
 519.48 1494.06 l 1,95,96
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   394
 434.047 1485.52 434.047 1485.52 368.437 1441.3 c 128,-1,97
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   395
 302.826 1397.07 302.826 1397.07 270.183 1335.19 c 128,-1,98
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   396
 237.54 1273.3 237.54 1273.3 237.54 1205.46 c 0,99,100
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   397
 237.54 1191.67 237.54 1191.67 238.654 1178 c 128,-1,101
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   398
 239.768 1164.33 239.768 1164.33 245.843 1138.32 c 128,-1,102
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   399
 251.919 1112.32 251.919 1112.32 262.355 1089.38 c 128,-1,103
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   400
 272.792 1066.44 272.792 1066.44 294.049 1038.29 c 128,-1,104
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   401
 315.306 1010.14 315.306 1010.14 343.997 987.711 c 128,-1,105
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   402
 372.688 965.283 372.688 965.283 418.059 944.776 c 128,-1,106
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   403
 463.429 924.268 463.429 924.268 519.48 912.42 c 1,94,-1
29073
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   404
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   405
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   406
StartChar: percent
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   407
Encoding: 37 37 8
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   408
Width: 1849
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   409
VWidth: 2220
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   410
Flags: W
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   411
HStem: -124.32 48.84<1414.14 1494.06> 721.5 48.84<1413.03 1495.17> 770.34 48.84<430.68 510.6> 1374.18 48.84<987.9 1106.67> 1616.16 48.84<429.57 486.18>
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   412
VStem: 124.32 137.64<1084.47 1348.65> 683.76 55.5<1098.9 1232.1> 1107.78 137.64<189.81 453.99> 1667.22 55.5<204.24 440.67>
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   413
Fore
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   414
1520.7 1580.64 m 2,0,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   415
 397.38 -91.0195 l 2,1,2
29085
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   416
 392.166 -98.3191 392.166 -98.3191 388.074 -103.86 c 128,-1,3
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   417
 383.981 -109.402 383.981 -109.402 380.472 -113.291 c 128,-1,4
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   418
 376.963 -117.181 376.963 -117.181 373.084 -119.632 c 128,-1,5
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   419
 369.205 -122.083 369.205 -122.083 364.418 -123.201 c 128,-1,6
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   420
 359.63 -124.32 359.63 -124.32 352.98 -124.32 c 0,7,8
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   421
 335.948 -124.32 335.948 -124.32 322.264 -111.093 c 128,-1,9
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   422
 308.58 -97.8649 308.58 -97.8649 308.58 -79.9199 c 0,10,11
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   423
 308.58 -64.3799 308.58 -64.3799 328.56 -35.5195 c 2,12,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   424
 1325.34 1449.66 l 1,13,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   425
 1323.12 1451.88 l 1,14,15
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   426
 1312.86 1445.04 1312.86 1445.04 1293.39 1435.41 c 128,-1,16
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   427
 1273.93 1425.78 1273.93 1425.78 1235.46 1410.28 c 128,-1,17
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   428
 1197 1394.79 1197 1394.79 1141.6 1384.49 c 128,-1,18
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   429
 1086.2 1374.18 1086.2 1374.18 1027.86 1374.18 c 0,19,20
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   430
 856.442 1374.18 856.442 1374.18 692.64 1467.42 c 1,21,22
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   431
 739.26 1351.98 739.26 1351.98 739.26 1216.56 c 0,23,24
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   432
 739.26 1094.03 739.26 1094.03 701.205 991.492 c 128,-1,25
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   433
 663.149 888.955 663.149 888.955 596.755 829.648 c 128,-1,26
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   434
 530.361 770.34 530.361 770.34 450.66 770.34 c 0,27,28
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   435
 388.323 770.34 388.323 770.34 329.444 803.135 c 128,-1,29
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   436
 270.565 835.93 270.565 835.93 225.036 893.326 c 128,-1,30
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   437
 179.507 950.723 179.507 950.723 151.914 1035.89 c 128,-1,31
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   438
 124.32 1121.05 124.32 1121.05 124.32 1218.78 c 0,32,33
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   439
 124.32 1313.52 124.32 1313.52 151.657 1397.64 c 128,-1,34
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   440
 178.995 1481.75 178.995 1481.75 224.148 1539.74 c 128,-1,35
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   441
 269.301 1597.72 269.301 1597.72 328.564 1631.36 c 128,-1,36
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   442
 387.827 1665 387.827 1665 450.66 1665 c 0,37,38
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   443
 499.122 1665 499.122 1665 535.867 1646.43 c 128,-1,39
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   444
 572.612 1627.86 572.612 1627.86 610.5 1593.96 c 0,40,41
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   445
 791.301 1423.02 791.301 1423.02 1025.64 1423.02 c 0,42,43
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   446
 1292.37 1423.02 1292.37 1423.02 1447.44 1633.92 c 0,44,45
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   447
 1451.64 1638.64 1451.64 1638.64 1455.27 1643.12 c 128,-1,46
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   448
 1458.91 1647.59 1458.91 1647.59 1463.21 1651.57 c 128,-1,47
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   449
 1467.52 1655.55 1467.52 1655.55 1471.9 1658.54 c 128,-1,48
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   450
 1476.27 1661.52 1476.27 1661.52 1481.97 1663.26 c 128,-1,49
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   451
 1487.66 1665 1487.66 1665 1494.06 1665 c 0,50,51
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   452
 1512.38 1665 1512.38 1665 1525.42 1651.96 c 128,-1,52
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   453
 1538.46 1638.91 1538.46 1638.91 1538.46 1620.6 c 0,53,54
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   454
 1538.46 1607.28 1538.46 1607.28 1520.7 1580.64 c 2,0,-1
29085
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   455
452.88 819.18 m 0,55,56
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   456
 543.583 819.18 543.583 819.18 613.671 932.4 c 128,-1,57
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   457
 683.76 1045.62 683.76 1045.62 683.76 1218.78 c 0,58,59
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   458
 683.76 1303.65 683.76 1303.65 664.195 1378.79 c 128,-1,60
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   459
 644.63 1453.92 644.63 1453.92 612.478 1505.31 c 128,-1,61
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   460
 580.326 1556.69 580.326 1556.69 538.557 1586.43 c 128,-1,62
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   461
 496.789 1616.16 496.789 1616.16 452.88 1616.16 c 0,63,64
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   462
 440.367 1616.16 440.367 1616.16 427.444 1613.71 c 128,-1,65
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   463
 414.521 1611.25 414.521 1611.25 394.823 1601.57 c 128,-1,66
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   464
 375.125 1591.88 375.125 1591.88 357.983 1575.84 c 128,-1,67
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   465
 340.842 1559.81 340.842 1559.81 322.605 1529.26 c 128,-1,68
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   466
 304.368 1498.7 304.368 1498.7 291.474 1458.14 c 128,-1,69
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   467
 278.58 1417.58 278.58 1417.58 270.27 1355.2 c 128,-1,70
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   468
 261.96 1292.83 261.96 1292.83 261.96 1216.56 c 0,71,72
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   469
 261.96 1140.78 261.96 1140.78 270.383 1078.74 c 128,-1,73
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   470
 278.806 1016.7 278.806 1016.7 291.866 976.391 c 128,-1,74
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   471
 304.926 936.082 304.926 936.082 323.301 905.671 c 128,-1,75
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   472
 341.675 875.26 341.675 875.26 358.919 859.32 c 128,-1,76
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   473
 376.163 843.38 376.163 843.38 395.79 833.725 c 128,-1,77
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   474
 415.418 824.07 415.418 824.07 428.147 821.625 c 128,-1,78
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   475
 440.876 819.18 440.876 819.18 452.88 819.18 c 0,55,56
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   476
1436.34 -75.4805 m 0,79,80
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   477
 1527.04 -75.4805 1527.04 -75.4805 1597.13 37.7398 c 128,-1,81
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   478
 1667.22 150.96 1667.22 150.96 1667.22 324.12 c 0,82,83
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   479
 1667.22 408.99 1667.22 408.99 1647.66 484.126 c 128,-1,84
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   480
 1628.09 559.262 1628.09 559.262 1595.94 610.646 c 128,-1,85
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   481
 1563.79 662.031 1563.79 662.031 1522.02 691.765 c 128,-1,86
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   482
 1480.25 721.5 1480.25 721.5 1436.34 721.5 c 0,87,88
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   483
 1423.83 721.5 1423.83 721.5 1410.9 719.047 c 128,-1,89
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   484
 1397.98 716.594 1397.98 716.594 1378.28 706.905 c 128,-1,90
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   485
 1358.58 697.217 1358.58 697.217 1341.44 681.184 c 128,-1,91
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   486
 1324.3 665.151 1324.3 665.151 1306.06 634.596 c 128,-1,92
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   487
 1287.83 604.042 1287.83 604.042 1274.93 563.479 c 128,-1,93
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   488
 1262.04 522.915 1262.04 522.915 1253.73 460.544 c 128,-1,94
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   489
 1245.42 398.172 1245.42 398.172 1245.42 321.9 c 0,95,96
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   490
 1245.42 246.122 1245.42 246.122 1253.84 184.081 c 128,-1,97
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   491
 1262.27 122.039 1262.27 122.039 1275.33 81.7307 c 128,-1,98
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   492
 1288.39 41.4221 1288.39 41.4221 1306.76 11.0108 c 128,-1,99
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   493
 1325.14 -19.4006 1325.14 -19.4006 1342.38 -35.3406 c 128,-1,100
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   494
 1359.62 -51.2807 1359.62 -51.2807 1379.25 -60.9356 c 128,-1,101
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   495
 1398.88 -70.5905 1398.88 -70.5905 1411.61 -73.0355 c 128,-1,102
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   496
 1424.34 -75.4805 1424.34 -75.4805 1436.34 -75.4805 c 0,79,80
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   497
1722.72 321.9 m 0,103,104
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   498
 1722.72 199.369 1722.72 199.369 1684.66 96.8321 c 128,-1,105
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   499
 1646.61 -5.70465 1646.61 -5.70465 1580.22 -65.0125 c 128,-1,106
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   500
 1513.82 -124.32 1513.82 -124.32 1434.12 -124.32 c 0,107,108
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   501
 1371.78 -124.32 1371.78 -124.32 1312.9 -91.5251 c 128,-1,109
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   502
 1254.03 -58.7299 1254.03 -58.7299 1208.5 -1.33373 c 128,-1,110
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   503
 1162.97 56.0625 1162.97 56.0625 1135.37 141.228 c 128,-1,111
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   504
 1107.78 226.394 1107.78 226.394 1107.78 324.12 c 0,112,113
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   505
 1107.78 418.857 1107.78 418.857 1135.12 502.976 c 128,-1,114
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   506
 1162.45 587.094 1162.45 587.094 1207.61 645.077 c 128,-1,115
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   507
 1252.76 703.06 1252.76 703.06 1312.02 736.7 c 128,-1,116
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   508
 1371.29 770.34 1371.29 770.34 1434.12 770.34 c 0,117,118
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   509
 1512.14 770.34 1512.14 770.34 1578.31 712.082 c 128,-1,119
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   510
 1644.49 653.825 1644.49 653.825 1683.61 550.358 c 128,-1,120
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   511
 1722.72 446.89 1722.72 446.89 1722.72 321.9 c 0,103,104
29073
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   512
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   513
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   514
StartChar: ampersand
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   515
Encoding: 38 38 9
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   516
Width: 1724
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   517
VWidth: 2220
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   518
Flags: W
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   519
HStem: -48.84 68.82<420.69 543.9 1236.54 1346.43> 888 68.82<1127.76 1127.76 1613.94 1613.94> 1540.68 48.84<629.37 734.82>
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   520
VStem: 93.24 184.26<295.26 344.1> 361.86 139.86<1248.75 1349.76> 801.42 55.5<1232.1 1307.58> 1538.46 62.16
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   521
Fore
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   522
1545.12 268.62 m 1,0,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   523
 1600.62 268.62 l 1,1,2
29085
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   524
 1597.35 128.136 1597.35 128.136 1507.09 39.6481 c 128,-1,3
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   525
 1416.84 -48.8398 1416.84 -48.8398 1287.6 -48.8398 c 0,4,5
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   526
 1090.91 -48.8398 1090.91 -48.8398 896.88 119.88 c 1,6,7
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   527
 707.709 -48.8398 707.709 -48.8398 495.06 -48.8398 c 0,8,9
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   528
 385.922 -48.8398 385.922 -48.8398 294.061 -6.36538 c 128,-1,10
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   529
 202.199 36.1091 202.199 36.1091 147.72 112.925 c 128,-1,11
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   530
 93.2402 189.741 93.2402 189.741 93.2402 284.16 c 0,12,13
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   531
 93.2402 319.439 93.2402 319.439 100.996 350.661 c 128,-1,14
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   532
 108.753 381.883 108.753 381.883 118.997 404.832 c 128,-1,15
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   533
 129.241 427.781 129.241 427.781 153.175 458.216 c 128,-1,16
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   534
 177.109 488.65 177.109 488.65 195.152 508.124 c 128,-1,17
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   535
 213.195 527.597 213.195 527.597 250.86 566.1 c 2,18,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   536
 452.88 781.44 l 1,19,20
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   537
 361.86 1012.89 361.86 1012.89 361.86 1232.1 c 0,21,22
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   538
 361.86 1316.63 361.86 1316.63 389.458 1386.6 c 128,-1,23
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   539
 417.055 1456.58 417.055 1456.58 461.427 1499.67 c 128,-1,24
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   540
 505.799 1542.77 505.799 1542.77 558.316 1566.15 c 128,-1,25
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   541
 610.833 1589.52 610.833 1589.52 663.78 1589.52 c 0,26,27
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   542
 708.823 1589.52 708.823 1589.52 744.156 1569.23 c 128,-1,28
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   543
 779.489 1548.95 779.489 1548.95 800.094 1518.43 c 128,-1,29
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   544
 820.7 1487.91 820.7 1487.91 834.092 1447.76 c 128,-1,30
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   545
 847.484 1407.61 847.484 1407.61 852.202 1372.44 c 128,-1,31
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   546
 856.92 1337.28 856.92 1337.28 856.92 1303.14 c 0,32,33
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   547
 856.92 1267.79 856.92 1267.79 846.189 1229.54 c 128,-1,34
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   548
 835.458 1191.29 835.458 1191.29 812.336 1150.11 c 128,-1,35
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   549
 789.213 1108.93 789.213 1108.93 767.461 1075.17 c 128,-1,36
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   550
 745.71 1041.42 745.71 1041.42 708.571 996.356 c 128,-1,37
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   551
 671.433 951.296 671.433 951.296 648.774 925.24 c 128,-1,38
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   552
 626.115 899.183 626.115 899.183 586.08 854.7 c 1,39,40
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   553
 619.872 766.381 619.872 766.381 679.125 661.699 c 128,-1,41
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   554
 738.379 557.017 738.379 557.017 797.834 472.444 c 128,-1,42
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   555
 857.288 387.871 857.288 387.871 896.893 335.359 c 128,-1,43
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   556
 936.498 282.846 936.498 282.846 954.6 261.96 c 1,44,45
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   557
 1097.56 438.164 1097.56 438.164 1272.06 745.92 c 1,46,47
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   558
 1272.37 746.862 1272.37 746.862 1276.21 754.548 c 128,-1,48
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   559
 1280.04 762.234 1280.04 762.234 1282.71 771.332 c 128,-1,49
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   560
 1285.38 780.43 1285.38 780.43 1285.38 790.32 c 0,50,51
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   561
 1285.38 833.385 1285.38 833.385 1243.77 860.692 c 128,-1,52
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   562
 1202.16 888 1202.16 888 1127.76 888 c 1,53,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   563
 1127.76 956.82 l 1,54,55
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   564
 1217.66 950.16 1217.66 950.16 1398.6 950.16 c 0,56,57
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   565
 1490.74 950.16 1490.74 950.16 1613.94 956.82 c 1,58,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   566
 1613.94 888 l 1,59,60
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   567
 1581.2 887.632 1581.2 887.632 1553.16 884.047 c 128,-1,61
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   568
 1525.12 880.461 1525.12 880.461 1502.74 875.838 c 128,-1,62
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   569
 1480.36 871.215 1480.36 871.215 1459.36 860.44 c 128,-1,63
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   570
 1438.36 849.664 1438.36 849.664 1423.45 841.323 c 128,-1,64
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   571
 1408.53 832.982 1408.53 832.982 1391.43 815.126 c 128,-1,65
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   572
 1374.34 797.27 1374.34 797.27 1363.74 785.32 c 128,-1,66
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   573
 1353.14 773.371 1353.14 773.371 1336.81 748.544 c 128,-1,67
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   574
 1320.47 723.717 1320.47 723.717 1311.05 708.269 c 128,-1,68
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   575
 1301.63 692.82 1301.63 692.82 1283.16 661.56 c 0,69,70
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   576
 1218.89 551.175 1218.89 551.175 1181.82 489.882 c 128,-1,71
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   577
 1144.75 428.59 1144.75 428.59 1091.46 350.757 c 128,-1,72
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   578
 1038.17 272.924 1038.17 272.924 990.12 217.56 c 1,73,74
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   579
 1156.5 19.9805 1156.5 19.9805 1296.48 19.9805 c 0,75,76
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   580
 1335.97 19.9805 1335.97 19.9805 1376.9 34.707 c 128,-1,77
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   581
 1417.82 49.4335 1417.82 49.4335 1455.41 77.9935 c 128,-1,78
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   582
 1492.99 106.553 1492.99 106.553 1517.87 156.321 c 128,-1,79
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   583
 1542.75 206.089 1542.75 206.089 1545.12 268.62 c 1,0,-1
29085
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   584
568.32 907.98 m 1,80,81
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   585
 801.42 1160.51 801.42 1160.51 801.42 1305.36 c 0,82,83
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   586
 801.42 1311.25 801.42 1311.25 801.128 1320.15 c 128,-1,84
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   587
 800.835 1329.05 800.835 1329.05 798.217 1353.6 c 128,-1,85
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   588
 795.599 1378.15 795.599 1378.15 791.031 1400.2 c 128,-1,86
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   589
 786.462 1422.25 786.462 1422.25 776.47 1449.1 c 128,-1,87
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   590
 766.478 1475.96 766.478 1475.96 752.974 1495.16 c 128,-1,88
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   591
 739.469 1514.36 739.469 1514.36 717.443 1527.52 c 128,-1,89
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   592
 695.416 1540.68 695.416 1540.68 668.22 1540.68 c 0,90,91
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   593
 637.604 1540.68 637.604 1540.68 609.178 1526.16 c 128,-1,92
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   594
 580.752 1511.64 580.752 1511.64 556.078 1482.36 c 128,-1,93
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   595
 531.405 1453.07 531.405 1453.07 516.562 1401.56 c 128,-1,94
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   596
 501.72 1350.05 501.72 1350.05 501.72 1283.16 c 0,95,96
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   597
 501.72 1105.31 501.72 1105.31 568.32 907.98 c 1,80,81
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   598
472.86 730.38 m 1,97,98
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   599
 429.755 688.871 429.755 688.871 405.632 663.514 c 128,-1,99
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   600
 381.509 638.156 381.509 638.156 353.182 601.016 c 128,-1,100
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   601
 324.856 563.877 324.856 563.877 310.864 530.917 c 128,-1,101
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   602
 296.872 497.957 296.872 497.957 287.186 452.969 c 128,-1,102
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   603
 277.5 407.98 277.5 407.98 277.5 355.2 c 0,103,104
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   604
 277.5 315.975 277.5 315.975 284.001 274.051 c 128,-1,105
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   605
 290.502 232.128 290.502 232.128 307.549 185.667 c 128,-1,106
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   606
 324.595 139.206 324.595 139.206 350.104 103.2 c 128,-1,107
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   607
 375.613 67.1938 375.613 67.1938 417.874 43.5871 c 128,-1,108
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   608
 460.135 19.9805 460.135 19.9805 512.82 19.9805 c 0,109,110
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   609
 541.868 19.9805 541.868 19.9805 573.989 24.875 c 128,-1,111
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   610
 606.109 29.7694 606.109 29.7694 652.285 43.0782 c 128,-1,112
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   611
 698.46 56.3869 698.46 56.3869 751.588 86.965 c 128,-1,113
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   612
 804.717 117.543 804.717 117.543 854.7 162.06 c 1,114,115
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   613
 767.623 249.137 767.623 249.137 650.46 421.8 c 0,116,117
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   614
 584.324 517.159 584.324 517.159 549.482 579.142 c 128,-1,118
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   615
 514.639 641.126 514.639 641.126 472.86 730.38 c 1,97,98
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   616
EndSplineSet
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   617
EndChar
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   618
StartChar: quotesingle
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   619
Encoding: 39 39 10
29085
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   620
Width: 610
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   621
VWidth: 2630
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   622
Flags: HW
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   623
HStem: 509.9 46.62<130.98 142.08> 1606.58 44.4<412.92 488.4>
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   624
VStem: 64.38 517.26
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   625
Fore
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   626
566.1 1473.38 m 2,0,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   627
 168.72 540.98 l 2,1,2
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   628
 155.4 509.9 155.4 509.9 139.86 509.9 c 0,3,4
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   629
 121.434 509.9 121.434 509.9 92.9072 521.787 c 128,-1,5
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   630
 64.3799 533.673 64.3799 533.673 64.3799 549.86 c 0,6,7
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   631
 64.3799 554.294 64.3799 554.294 71.04 580.94 c 2,8,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   632
 339.66 1548.86 l 2,9,10
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   633
 344.242 1563.75 344.242 1563.75 346.869 1571.28 c 128,-1,11
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   634
 349.496 1578.81 349.496 1578.81 359.25 1596.55 c 128,-1,12
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   635
 369.004 1614.29 369.004 1614.29 380.188 1624.07 c 128,-1,13
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   636
 391.37 1633.84 391.37 1633.84 411.749 1642.41 c 128,-1,14
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   637
 432.128 1650.98 432.128 1650.98 457.32 1650.98 c 0,15,16
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   638
 505.62 1650.98 505.62 1650.98 543.63 1617.5 c 128,-1,17
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   639
 581.64 1584.01 581.64 1584.01 581.64 1535.54 c 0,18,19
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   640
 581.64 1506.68 581.64 1506.68 566.1 1473.38 c 2,0,-1
29073
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   641
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   642
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   643
StartChar: parenleft
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   644
Encoding: 40 40 11
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   645
Width: 861
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   646
VWidth: 2220
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   647
Flags: W
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   648
HStem: -555 46.62<701.52 719.28> 1620.6 44.4<701.52 719.28>
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   649
VStem: 219.78 128.76<468.42 648.24>
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   650
Fore
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   651
734.82 -532.8 m 0,0,1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   652
 734.82 -555 734.82 -555 712.62 -555 c 0,2,3
29085
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   653
 702.684 -555 702.684 -555 666.995 -526.936 c 128,-1,4
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   654
 631.306 -498.872 631.306 -498.872 581.964 -449.968 c 128,-1,5
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   655
 532.621 -401.063 532.621 -401.063 472.606 -316.799 c 128,-1,6
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   656
 412.59 -232.535 412.59 -232.535 366.3 -137.64 c 0,7,8
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   657
 219.78 163.392 219.78 163.392 219.78 555 c 0,9,10
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   658
 219.78 930.442 219.78 930.442 359.64 1232.1 c 0,11,12
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   659
 396.592 1311.64 396.592 1311.64 444.208 1384.75 c 128,-1,13
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   660
 491.824 1457.85 491.824 1457.85 534.385 1506.92 c 128,-1,14
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   661
 576.947 1555.99 576.947 1555.99 616.196 1593.18 c 128,-1,15
29085
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   662
 655.446 1630.37 655.446 1630.37 680.266 1647.68 c 128,-1,16
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   663
 705.086 1665 705.086 1665 712.62 1665 c 0,17,18
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   664
 734.82 1665 734.82 1665 734.82 1642.8 c 0,19,20
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   665
 734.82 1638.61 734.82 1638.61 733.8 1635.81 c 128,-1,21
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   666
 732.78 1633.02 732.78 1633.02 726.221 1625.37 c 128,-1,22
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   667
 719.662 1617.71 719.662 1617.71 705.96 1605.06 c 0,23,24
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   668
 348.54 1241.83 348.54 1241.83 348.54 555 c 0,25,26
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   669
 348.54 446.414 348.54 446.414 357.863 343.002 c 128,-1,27
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   670
 367.185 239.59 367.185 239.59 391.592 123.482 c 128,-1,28
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   671
 415.998 7.37431 415.998 7.37431 454.228 -95.5992 c 128,-1,29
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   672
 492.458 -198.573 492.458 -198.573 554.558 -300.733 c 128,-1,30
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   673
 616.657 -402.893 616.657 -402.893 697.08 -483.96 c 0,31,32
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   674
 714.997 -501.877 714.997 -501.877 723.574 -512.058 c 128,-1,33
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   675
 732.152 -522.238 732.152 -522.238 733.486 -525.422 c 128,-1,34
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   676
 734.82 -528.606 734.82 -528.606 734.82 -532.8 c 0,0,1
29073
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   677
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   678
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   679
StartChar: parenright
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   680
Encoding: 41 41 12
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   681
Width: 861
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   682
VWidth: 2220
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   683
Flags: W
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   684
HStem: -555 46.62<142.08 159.84> 1620.6 44.4<142.08 159.84>
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   685
VStem: 512.82 128.76<461.76 641.58>
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   686
Fore
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   687
641.58 555 m 0,0,1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   688
 641.58 179.557 641.58 179.557 501.72 -122.1 c 0,2,3
29085
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   689
 464.767 -201.642 464.767 -201.642 417.152 -274.746 c 128,-1,4
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   690
 369.536 -347.851 369.536 -347.851 326.975 -396.919 c 128,-1,5
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   691
 284.414 -445.987 284.414 -445.987 245.164 -483.178 c 128,-1,6
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   692
 205.914 -520.369 205.914 -520.369 181.094 -537.685 c 128,-1,7
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   693
 156.274 -555 156.274 -555 148.74 -555 c 0,8,9
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   694
 138.75 -555 138.75 -555 132.645 -548.895 c 128,-1,10
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   695
 126.54 -542.79 126.54 -542.79 126.54 -532.8 c 0,11,12
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   696
 126.54 -528.606 126.54 -528.606 127.56 -525.815 c 128,-1,13
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   697
 128.581 -523.023 128.581 -523.023 135.14 -515.365 c 128,-1,14
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   698
 141.699 -507.707 141.699 -507.707 155.4 -495.06 c 0,15,16
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   699
 512.82 -131.874 512.82 -131.874 512.82 555 c 0,17,18
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   700
 512.82 897.818 512.82 897.818 423.685 1161.02 c 128,-1,19
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   701
 334.55 1424.22 334.55 1424.22 168.72 1591.74 c 0,20,21
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   702
 148.695 1610.71 148.695 1610.71 139.109 1621.4 c 128,-1,22
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   703
 129.523 1632.08 129.523 1632.08 128.031 1635.34 c 128,-1,23
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   704
 126.54 1638.61 126.54 1638.61 126.54 1642.8 c 0,24,25
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   705
 126.54 1652.79 126.54 1652.79 132.645 1658.9 c 128,-1,26
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   706
 138.75 1665 138.75 1665 148.74 1665 c 128,-1,27
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   707
 158.677 1665 158.677 1665 194.366 1636.94 c 128,-1,28
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   708
 230.055 1608.87 230.055 1608.87 279.397 1559.97 c 128,-1,29
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   709
 328.739 1511.06 328.739 1511.06 388.754 1426.8 c 128,-1,30
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   710
 448.769 1342.54 448.769 1342.54 495.06 1247.64 c 0,31,32
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   711
 641.58 946.609 641.58 946.609 641.58 555 c 0,0,1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   712
EndSplineSet
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   713
EndChar
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   714
StartChar: asterisk
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   715
Encoding: 42 42 13
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   716
Width: 1110
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   717
VWidth: 2220
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   718
Flags: W
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   719
HStem: 708.18 46.62<538.35 570.54> 1620.6 44.4<537.24 569.43>
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   720
VStem: 144.3 819.18<976.8 991.23 964.59 992.34 1381.95 1408.59>
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   721
Fore
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   722
603.84 1185.48 m 1,0,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   723
 916.86 1038.96 l 2,1,2
29085
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   724
 943.732 1026.31 943.732 1026.31 953.606 1012.49 c 128,-1,3
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   725
 963.48 998.667 963.48 998.667 963.48 979.02 c 0,4,5
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   726
 963.48 955.958 963.48 955.958 946.204 936.409 c 128,-1,6
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   727
 928.928 916.86 928.928 916.86 903.54 916.86 c 0,7,8
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   728
 895.351 916.86 895.351 916.86 888.905 918.833 c 128,-1,9
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   729
 882.458 920.807 882.458 920.807 878.216 923.766 c 128,-1,10
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   730
 873.973 926.726 873.973 926.726 868.02 930.18 c 0,11,12
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   731
 862.768 933.331 862.768 933.331 750.071 1016.34 c 128,-1,13
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   732
 637.374 1099.35 637.374 1099.35 579.42 1141.08 c 1,14,15
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   733
 612.72 774.819 612.72 774.819 612.72 763.68 c 0,16,17
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   734
 612.72 741.319 612.72 741.319 595.702 724.75 c 128,-1,18
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   735
 578.685 708.18 578.685 708.18 552.78 708.18 c 0,19,20
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   736
 530.104 708.18 530.104 708.18 512.582 723.905 c 128,-1,21
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   737
 495.06 739.63 495.06 739.63 495.06 763.68 c 2,22,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   738
 528.36 1141.08 l 1,23,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   739
 217.56 916.86 l 1,24,25
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   740
 196.991 916.86 196.991 916.86 181.948 923.165 c 128,-1,26
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   741
 166.906 929.47 166.906 929.47 159.984 937.195 c 128,-1,27
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   742
 153.063 944.921 153.063 944.921 149.128 955.488 c 128,-1,28
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   743
 145.193 966.055 145.193 966.055 144.746 970.584 c 128,-1,29
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   744
 144.3 975.112 144.3 975.112 144.3 979.02 c 0,30,31
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   745
 144.3 1000.01 144.3 1000.01 154.625 1013.39 c 128,-1,32
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   746
 164.949 1026.78 164.949 1026.78 195.36 1041.18 c 2,33,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   747
 503.94 1187.7 l 1,34,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   748
 190.92 1334.22 l 2,35,36
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   749
 164.048 1346.87 164.048 1346.87 154.174 1360.69 c 128,-1,37
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   750
 144.3 1374.51 144.3 1374.51 144.3 1394.16 c 0,38,39
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   751
 144.3 1417.22 144.3 1417.22 161.576 1436.77 c 128,-1,40
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   752
 178.852 1456.32 178.852 1456.32 204.24 1456.32 c 0,41,42
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   753
 215.34 1456.32 215.34 1456.32 223.332 1452.66 c 128,-1,43
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   754
 231.324 1448.99 231.324 1448.99 253.08 1431.9 c 2,44,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   755
 528.36 1232.1 l 1,45,46
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   756
 495.06 1598.38 495.06 1598.38 495.06 1609.5 c 0,47,48
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   757
 495.06 1631.86 495.06 1631.86 512.077 1648.43 c 128,-1,49
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   758
 529.095 1665 529.095 1665 555 1665 c 0,50,51
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   759
 577.676 1665 577.676 1665 595.198 1649.27 c 128,-1,52
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   760
 612.72 1633.55 612.72 1633.55 612.72 1609.5 c 2,53,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   761
 579.42 1232.1 l 1,54,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   762
 825.84 1414.14 l 2,55,56
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   763
 866.506 1443.86 866.506 1443.86 878.64 1450.09 c 128,-1,57
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   764
 890.775 1456.32 890.775 1456.32 903.54 1456.32 c 0,58,59
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   765
 928.928 1456.32 928.928 1456.32 946.204 1436.77 c 128,-1,60
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   766
 963.48 1417.22 963.48 1417.22 963.48 1394.16 c 0,61,62
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   767
 963.48 1373.17 963.48 1373.17 953.156 1359.79 c 128,-1,63
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   768
 942.831 1346.41 942.831 1346.41 912.42 1332 c 2,64,-1
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   769
 603.84 1185.48 l 1,0,-1
29073
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   770
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   771
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   772
StartChar: plus
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   773
Encoding: 43 43 14
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   774
Width: 1724
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   775
VWidth: 2220
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   776
Flags: W
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   777
HStem: -184.26 46.62<841.38 885.78> 510.6 88.8<197.58 819.18 907.98 1527.36> 1249.86 44.4<841.38 885.78>
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   778
VStem: 819.18 88.8<-111 510.6 599.4 1221>
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   779
Fore
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   780
907.98 510.6 m 1,0,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   781
 907.98 -111 l 2,1,2
29085
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   782
 907.98 -127.234 907.98 -127.234 907.131 -136.322 c 128,-1,3
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   783
 906.282 -145.41 906.282 -145.41 902.586 -158.522 c 128,-1,4
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   784
 898.889 -171.634 898.889 -171.634 889.094 -177.947 c 128,-1,5
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   785
 879.298 -184.26 879.298 -184.26 863.58 -184.26 c 128,-1,6
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   786
 847.862 -184.26 847.862 -184.26 838.067 -177.947 c 128,-1,7
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   787
 828.271 -171.634 828.271 -171.634 824.574 -158.522 c 128,-1,8
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   788
 820.878 -145.41 820.878 -145.41 820.029 -136.322 c 128,-1,9
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   789
 819.18 -127.234 819.18 -127.234 819.18 -111 c 2,10,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   790
 819.18 510.6 l 1,11,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   791
 197.58 510.6 l 2,12,13
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   792
 181.346 510.6 181.346 510.6 172.258 511.449 c 128,-1,14
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   793
 163.17 512.298 163.17 512.298 150.058 515.994 c 128,-1,15
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   794
 136.946 519.691 136.946 519.691 130.633 529.486 c 128,-1,16
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   795
 124.32 539.282 124.32 539.282 124.32 555 c 128,-1,17
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   796
 124.32 570.718 124.32 570.718 130.633 580.514 c 128,-1,18
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   797
 136.946 590.309 136.946 590.309 150.058 594.006 c 128,-1,19
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   798
 163.17 597.702 163.17 597.702 172.258 598.551 c 128,-1,20
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   799
 181.346 599.4 181.346 599.4 197.58 599.4 c 2,21,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   800
 819.18 599.4 l 1,22,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   801
 819.18 1221 l 2,23,24
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   802
 819.18 1237.23 819.18 1237.23 820.029 1246.32 c 128,-1,25
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   803
 820.878 1255.41 820.878 1255.41 824.574 1268.52 c 128,-1,26
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   804
 828.271 1281.63 828.271 1281.63 838.067 1287.95 c 128,-1,27
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   805
 847.862 1294.26 847.862 1294.26 863.58 1294.26 c 128,-1,28
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   806
 879.298 1294.26 879.298 1294.26 889.094 1287.95 c 128,-1,29
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   807
 898.889 1281.63 898.889 1281.63 902.586 1268.52 c 128,-1,30
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   808
 906.282 1255.41 906.282 1255.41 907.131 1246.32 c 128,-1,31
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   809
 907.98 1237.23 907.98 1237.23 907.98 1221 c 2,32,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   810
 907.98 599.4 l 1,33,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   811
 1527.36 599.4 l 2,34,35
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   812
 1543.59 599.4 1543.59 599.4 1552.68 598.551 c 128,-1,36
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   813
 1561.77 597.702 1561.77 597.702 1574.88 594.006 c 128,-1,37
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   814
 1587.99 590.309 1587.99 590.309 1594.31 580.514 c 128,-1,38
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   815
 1600.62 570.718 1600.62 570.718 1600.62 555 c 128,-1,39
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   816
 1600.62 539.282 1600.62 539.282 1594.31 529.486 c 128,-1,40
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   817
 1587.99 519.691 1587.99 519.691 1574.88 515.994 c 128,-1,41
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   818
 1561.77 512.298 1561.77 512.298 1552.68 511.449 c 128,-1,42
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   819
 1543.59 510.6 1543.59 510.6 1527.36 510.6 c 2,43,-1
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   820
 907.98 510.6 l 1,0,-1
29073
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   821
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   822
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   823
StartChar: comma
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   824
Encoding: 44 44 15
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   825
Width: 614
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   826
VWidth: 2220
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   827
Flags: W
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   828
HStem: -428.46 46.62<243.09 261.96> 0 235.32<269.73 326.34>
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   829
VStem: 401.82 48.84<-68.82 17.76>
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   830
Fore
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   831
397.38 35.5195 m 1,0,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   832
 392.94 31.0801 l 2,1,2
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   833
 354.089 0 354.089 0 308.58 0 c 0,3,4
29085
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   834
 252.317 0 252.317 0 221.618 35.0841 c 128,-1,5
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   835
 190.92 70.1682 190.92 70.1682 190.92 117.66 c 0,6,7
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   836
 190.92 164.679 190.92 164.679 222.267 200 c 128,-1,8
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   837
 253.614 235.32 253.614 235.32 308.58 235.32 c 0,9,10
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   838
 374.785 235.32 374.785 235.32 412.722 172.378 c 128,-1,11
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   839
 450.66 109.436 450.66 109.436 450.66 2.21973 c 0,12,13
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   840
 450.66 -69.7755 450.66 -69.7755 432.26 -139.984 c 128,-1,14
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   841
 413.86 -210.193 413.86 -210.193 387.169 -260.291 c 128,-1,15
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   842
 360.477 -310.39 360.477 -310.39 331.312 -349.765 c 128,-1,16
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   843
 302.147 -389.14 302.147 -389.14 279.827 -408.8 c 128,-1,17
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   844
 257.507 -428.46 257.507 -428.46 248.64 -428.46 c 128,-1,18
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   845
 239.76 -428.46 239.76 -428.46 233.1 -421.8 c 128,-1,19
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   846
 226.44 -415.14 226.44 -415.14 226.44 -404.04 c 0,20,21
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   847
 226.44 -397.658 226.44 -397.658 228.938 -393.911 c 128,-1,22
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   848
 231.435 -390.165 231.435 -390.165 241.98 -379.62 c 0,23,24
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   849
 317.105 -299.373 317.105 -299.373 359.463 -200.68 c 128,-1,25
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   850
 401.82 -101.987 401.82 -101.987 401.82 2.21973 c 0,26,27
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   851
 401.82 35.5195 401.82 35.5195 397.38 35.5195 c 1,0,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   852
EndSplineSet
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   853
EndChar
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   854
StartChar: hyphen
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   855
Encoding: 45 45 16
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   856
Width: 1724
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   857
VWidth: 2220
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   858
Flags: W
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   859
HStem: 510.6 88.8<241.98 1467.42 257.52 1467.42>
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   860
VStem: 184.26 1356.42<532.8 577.2>
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   861
Fore
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   862
1467.42 510.6 m 2,0,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   863
 257.52 510.6 l 2,1,2
29085
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   864
 241.286 510.6 241.286 510.6 232.198 511.449 c 128,-1,3
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   865
 223.11 512.298 223.11 512.298 209.998 515.994 c 128,-1,4
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   866
 196.886 519.691 196.886 519.691 190.573 529.486 c 128,-1,5
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   867
 184.26 539.282 184.26 539.282 184.26 555 c 128,-1,6
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   868
 184.26 570.718 184.26 570.718 190.573 580.514 c 128,-1,7
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   869
 196.886 590.309 196.886 590.309 209.998 594.006 c 128,-1,8
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   870
 223.11 597.702 223.11 597.702 232.198 598.551 c 128,-1,9
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   871
 241.286 599.4 241.286 599.4 257.52 599.4 c 2,10,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   872
 1467.42 599.4 l 2,11,12
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   873
 1483.65 599.4 1483.65 599.4 1492.74 598.551 c 128,-1,13
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   874
 1501.83 597.702 1501.83 597.702 1514.94 594.006 c 128,-1,14
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   875
 1528.05 590.309 1528.05 590.309 1534.37 580.514 c 128,-1,15
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   876
 1540.68 570.718 1540.68 570.718 1540.68 555 c 128,-1,16
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   877
 1540.68 539.282 1540.68 539.282 1534.37 529.486 c 128,-1,17
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   878
 1528.05 519.691 1528.05 519.691 1514.94 515.994 c 128,-1,18
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   879
 1501.83 512.298 1501.83 512.298 1492.74 511.449 c 128,-1,19
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   880
 1483.65 510.6 1483.65 510.6 1467.42 510.6 c 2,0,-1
29073
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   881
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   882
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   883
StartChar: period
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   884
Encoding: 46 46 17
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   885
Width: 614
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   886
VWidth: 2220
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   887
Flags: W
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   888
HStem: 0 235.32<276.39 340.77>
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   889
VStem: 190.92 235.32<85.47 149.85>
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   890
Fore
29085
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   891
426.24 117.66 m 128,-1,1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   892
 426.24 69.3752 426.24 69.3752 391.553 34.6876 c 128,-1,2
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   893
 356.865 0 356.865 0 308.58 0 c 128,-1,3
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   894
 260.295 0 260.295 0 225.608 34.6876 c 128,-1,4
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   895
 190.92 69.3752 190.92 69.3752 190.92 117.66 c 128,-1,5
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   896
 190.92 165.945 190.92 165.945 225.608 200.633 c 128,-1,6
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   897
 260.295 235.32 260.295 235.32 308.58 235.32 c 128,-1,7
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   898
 356.865 235.32 356.865 235.32 391.553 200.633 c 128,-1,0
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   899
 426.24 165.945 426.24 165.945 426.24 117.66 c 128,-1,1
29073
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   900
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   901
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   902
StartChar: slash
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   903
Encoding: 47 47 18
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   904
Width: 1110
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   905
VWidth: 2220
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   906
Flags: W
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   907
HStem: -555 46.62<156.51 184.26> 1620.6 44.4
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   908
VStem: 124.32 859.14
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   909
Fore
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   910
972.36 1580.64 m 2,0,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   911
 215.34 -510.6 l 2,1,2
29085
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   912
 211.229 -524.304 211.229 -524.304 207.159 -532.526 c 128,-1,3
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   913
 203.089 -540.748 203.089 -540.748 193.181 -547.874 c 128,-1,4
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   914
 183.273 -555 183.273 -555 168.72 -555 c 0,5,6
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   915
 150.405 -555 150.405 -555 137.363 -541.957 c 128,-1,7
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   916
 124.32 -528.915 124.32 -528.915 124.32 -510.6 c 0,8,9
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   917
 124.32 -499.5 124.32 -499.5 135.42 -470.64 c 2,10,-1
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   918
 892.44 1620.6 l 2,11,12
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   919
 896.551 1634.3 896.551 1634.3 900.621 1642.53 c 128,-1,13
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   920
 904.691 1650.75 904.691 1650.75 914.599 1657.87 c 128,-1,14
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   921
 924.507 1665 924.507 1665 939.06 1665 c 0,15,16
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   922
 957.375 1665 957.375 1665 970.417 1651.96 c 128,-1,17
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
   923
 983.46 1638.91 983.46 1638.91 983.46 1620.6 c 0,18,19
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   924
 983.46 1609.5 983.46 1609.5 972.36 1580.64 c 2,0,-1
29073
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   925
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   926
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   927
StartChar: zero
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   928
Encoding: 48 48 19
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   929
Width: 1233
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   930
Flags: W
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   931
TtfInstrs: 266
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   932
5T0a$#niRG%$qfs*gn8g*ZG;,!#m*m*[)UN&H(n]eEdb70`VdGo^!.WeF#"Ueh7"V!A=L-""sd1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   933
"YU'5#;6?9#qlW=$U4VU!C$WM"$ZoQ"[<2U#<rJY#sSb]$Vpau!D`bm$;V%:!+,b6!ac:A$_IEk
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   934
!M9Fc".o^g"eQ!k#G29o$(hQs$a0Q6!NuR."0Vj2"g8-6#HnE:$*O]>$bl\V!P\]N"2=uR"ht8V
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   935
#JUPZ$,6h^$UucL0**^-0*<j10*O!50*a-90*s9=0+2+e?NFL8?NXX<?Njd@?O'pD?O:'H?OOUK
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   936
^B)(N^B;4R^BM@V^B_LZ^BqX^^C);m!F5[*
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   937
EndTtf
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   938
Fore
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   939
483 750 m 0,0,1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   940
 483 805 483 805 521.5 845 c 128,-1,2
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   941
 560 885 560 885 614 885 c 0,3,4
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   942
 670 885 670 885 710 845 c 128,-1,5
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   943
 750 805 750 805 750 750 c 0,6,7
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   944
 750 694 750 694 710.5 655 c 128,-1,8
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   945
 671 616 671 616 614 616 c 0,9,10
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   946
 558 616 558 616 520.5 654 c 128,-1,11
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   947
 483 692 483 692 483 750 c 0,0,1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   948
616 1360 m 0,12,13
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   949
 475 1360 475 1360 405.5 1208 c 128,-1,14
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   950
 336 1056 336 1056 336 745 c 0,15,16
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   951
 336 435 336 435 405.5 283 c 128,-1,17
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   952
 475 131 475 131 616 131 c 0,18,19
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   953
 758 131 758 131 827.5 283 c 128,-1,20
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   954
 897 435 897 435 897 745 c 0,21,22
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   955
 897 1056 897 1056 827.5 1208 c 128,-1,23
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   956
 758 1360 758 1360 616 1360 c 0,12,13
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   957
616 1520 m 256,24,25
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   958
 855 1520 855 1520 977.5 1324 c 128,-1,26
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   959
 1100 1128 1100 1128 1100 745 c 0,27,28
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   960
 1100 363 1100 363 977.5 167 c 128,-1,29
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   961
 855 -29 855 -29 616 -29 c 256,30,31
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   962
 377 -29 377 -29 255 167 c 128,-1,32
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   963
 133 363 133 363 133 745 c 0,33,34
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   964
 133 1128 133 1128 255 1324 c 128,-1,35
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   965
 377 1520 377 1520 616 1520 c 256,24,25
29073
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   966
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   967
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   968
StartChar: one
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   969
Encoding: 49 49 20
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   970
Width: 1233
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   971
Flags: W
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   972
TtfInstrs: 38
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   973
5SO<e"9OnnL^*pH#m_a[*WlBe!=KIgm)8hg0`Wln1A'q_lnAD>
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   974
EndTtf
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   975
Fore
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   976
270 170 m 1,0,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   977
 584 170 l 1,1,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   978
 584 1311 l 1,2,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   979
 246 1235 l 1,3,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   980
 246 1419 l 1,4,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   981
 582 1493 l 1,5,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   982
 784 1493 l 1,6,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   983
 784 170 l 1,7,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   984
 1094 170 l 1,8,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   985
 1094 0 l 1,9,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   986
 270 0 l 1,10,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   987
 270 170 l 1,0,-1
29073
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   988
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   989
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
   990
StartChar: two
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   991
Encoding: 50 50 21
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   992
Width: 1233
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   993
Flags: W
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   994
TtfInstrs: 81
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   995
5Uc[Q,m=JV(`=4o(E4Y)"pI=)&Z6))'UAk%QN@-u$3C58*Z$"3"!elur5AO"^q^Np3ACLeln\5"
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   996
oZT!^;cj89"mlm<3<p*!m2%N\+ohTC
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   997
EndTtf
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   998
Fore
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
   999
373 170 m 1,0,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1000
 1059 170 l 1,1,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1001
 1059 0 l 1,2,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1002
 152 0 l 1,3,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1003
 152 170 l 1,4,5
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1004
 339 367 339 367 479 518 c 128,-1,6
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1005
 619 669 619 669 672 731 c 0,7,8
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1006
 772 853 772 853 807 928.5 c 128,-1,9
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1007
 842 1004 842 1004 842 1083 c 0,10,11
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1008
 842 1208 842 1208 768.5 1279 c 128,-1,12
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1009
 695 1350 695 1350 567 1350 c 0,13,14
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1010
 476 1350 476 1350 376 1317 c 128,-1,15
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1011
 276 1284 276 1284 164 1217 c 1,16,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1012
 164 1421 l 1,17,18
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1013
 267 1470 267 1470 366.5 1495 c 128,-1,19
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1014
 466 1520 466 1520 563 1520 c 0,20,21
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1015
 782 1520 782 1520 915.5 1403.5 c 128,-1,22
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1016
 1049 1287 1049 1287 1049 1098 c 0,23,24
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1017
 1049 1002 1049 1002 1004.5 906 c 128,-1,25
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1018
 960 810 960 810 860 694 c 0,26,27
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1019
 804 629 804 629 697.5 514 c 128,-1,28
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1020
 591 399 591 399 373 170 c 1,0,-1
29073
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1021
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1022
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1023
StartChar: three
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1024
Encoding: 51 51 22
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1025
Width: 1233
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1026
Flags: W
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1027
TtfInstrs: 71
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1028
5Uc[HQPBjc$)S/u"s8aGVAtpIQ3N`lW@8Sr!!<oQ*[VF>"!Sg$#p1T-r5?POm*tA6(HF2M&FAKM
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1029
m.BWUme6&[mPus$
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1030
EndTtf
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1031
Fore
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1032
776 799 m 1,0,1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1033
 923 760 923 760 1001 660.5 c 128,-1,2
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1034
 1079 561 1079 561 1079 412 c 0,3,4
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1035
 1079 206 1079 206 940.5 88.5 c 128,-1,5
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1036
 802 -29 802 -29 557 -29 c 0,6,7
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1037
 454 -29 454 -29 347 -10 c 128,-1,8
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1038
 240 9 240 9 137 45 c 1,9,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1039
 137 246 l 1,10,11
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1040
 239 193 239 193 338 167 c 128,-1,12
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1041
 437 141 437 141 535 141 c 0,13,14
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1042
 701 141 701 141 790 216 c 128,-1,15
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1043
 879 291 879 291 879 432 c 0,16,17
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1044
 879 562 879 562 790 638.5 c 128,-1,18
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1045
 701 715 701 715 549 715 c 2,19,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1046
 395 715 l 1,20,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1047
 395 881 l 1,21,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1048
 549 881 l 2,22,23
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1049
 688 881 688 881 766 942 c 128,-1,24
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1050
 844 1003 844 1003 844 1112 c 0,25,26
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1051
 844 1227 844 1227 771.5 1288.5 c 128,-1,27
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1052
 699 1350 699 1350 565 1350 c 0,28,29
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1053
 476 1350 476 1350 381 1330 c 128,-1,30
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1054
 286 1310 286 1310 182 1270 c 1,31,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1055
 182 1456 l 1,32,33
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1056
 303 1488 303 1488 397.5 1504 c 128,-1,34
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1057
 492 1520 492 1520 565 1520 c 0,35,36
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1058
 783 1520 783 1520 913.5 1410.5 c 128,-1,37
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1059
 1044 1301 1044 1301 1044 1120 c 0,38,39
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1060
 1044 997 1044 997 975.5 915 c 128,-1,40
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1061
 907 833 907 833 776 799 c 1,0,1
29073
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1062
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1063
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1064
StartChar: four
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1065
Encoding: 52 52 23
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1066
Width: 1233
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1067
Flags: W
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1068
TtfInstrs: 66
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1069
5T^"9!t>54!t@Qs!t,@#"T\^]#ltGA!$2CK"qM+f%M8R9e3*(Q&NMQG0BCVFlnT260M>>H#7q$[
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1070
#7q'\=X!hG
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1071
EndTtf
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1072
Fore
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1073
735 1309 m 1,0,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1074
 264 520 l 1,1,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1075
 735 520 l 1,2,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1076
 735 1309 l 1,0,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1077
702 1493 m 1,3,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1078
 936 1493 l 1,4,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1079
 936 520 l 1,5,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1080
 1135 520 l 1,6,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1081
 1135 356 l 1,7,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1082
 936 356 l 1,8,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1083
 936 0 l 1,9,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1084
 735 0 l 1,10,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1085
 735 356 l 1,11,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1086
 102 356 l 1,12,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1087
 102 547 l 1,13,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1088
 702 1493 l 1,3,-1
29073
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1089
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1090
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1091
StartChar: five
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1092
Encoding: 53 53 24
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1093
Width: 1233
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1094
Flags: W
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1095
TtfInstrs: 61
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1096
5U$=9*?(7L&W73\'UK71QN2gNR0T`5"!.FY*WZTl!"^4n&H'KE`9\''0`VdGjRhdMme6&[rkoF0
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1097
0E;(Q
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1098
EndTtf
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1099
Fore
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1100
207 1493 m 1,0,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1101
 963 1493 l 1,1,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1102
 963 1323 l 1,2,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1103
 391 1323 l 1,3,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1104
 391 956 l 1,4,5
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1105
 434 972 434 972 477.5 979.5 c 128,-1,6
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1106
 521 987 521 987 565 987 c 0,7,8
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1107
 797 987 797 987 933 850 c 128,-1,9
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1108
 1069 713 1069 713 1069 479 c 0,10,11
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1109
 1069 243 1069 243 926.5 107 c 128,-1,12
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1110
 784 -29 784 -29 537 -29 c 0,13,14
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1111
 418 -29 418 -29 319.5 -13 c 128,-1,15
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1112
 221 3 221 3 143 35 c 1,16,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1113
 143 240 l 1,17,18
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1114
 235 190 235 190 328 165.5 c 128,-1,19
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1115
 421 141 421 141 518 141 c 0,20,21
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1116
 685 141 685 141 775.5 229 c 128,-1,22
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1117
 866 317 866 317 866 479 c 0,23,24
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1118
 866 639 866 639 772.5 728 c 128,-1,25
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1119
 679 817 679 817 512 817 c 0,26,27
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1120
 431 817 431 817 354 798.5 c 128,-1,28
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1121
 277 780 277 780 207 743 c 1,29,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1122
 207 1493 l 1,0,-1
29073
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1123
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1124
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1125
StartChar: six
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1126
Encoding: 54 54 25
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1127
Width: 1233
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1128
Flags: W
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1129
TtfInstrs: 61
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1130
5U-LU)4([PQOjM)"9FD\NWb[aQ4TH1+s$_2%3c#]*!$]p,nU"@m/5r20`VdGo^)5:&EOJk&FL,j
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1131
0E;(Q
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1132
EndTtf
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1133
Fore
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1134
991 1460 m 1,0,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1135
 991 1274 l 1,1,2
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1136
 928 1311 928 1311 857 1330.5 c 128,-1,3
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1137
 786 1350 786 1350 709 1350 c 0,4,5
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1138
 517 1350 517 1350 418 1205.5 c 128,-1,6
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1139
 319 1061 319 1061 319 780 c 1,7,8
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1140
 367 880 367 880 452 933.5 c 128,-1,9
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1141
 537 987 537 987 647 987 c 0,10,11
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1142
 863 987 863 987 981.5 854.5 c 128,-1,12
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1143
 1100 722 1100 722 1100 479 c 0,13,14
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1144
 1100 237 1100 237 978 104 c 128,-1,15
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1145
 856 -29 856 -29 635 -29 c 0,16,17
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1146
 375 -29 375 -29 254 157.5 c 128,-1,18
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1147
 133 344 133 344 133 745 c 0,19,20
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1148
 133 1123 133 1123 278.5 1321.5 c 128,-1,21
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1149
 424 1520 424 1520 700 1520 c 0,22,23
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1150
 774 1520 774 1520 848 1504.5 c 128,-1,24
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1151
 922 1489 922 1489 991 1460 c 1,0,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1152
631 829 m 0,25,26
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1153
 502 829 502 829 428 736 c 128,-1,27
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1154
 354 643 354 643 354 479 c 256,28,29
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1155
 354 315 354 315 428 222 c 128,-1,30
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1156
 502 129 502 129 631 129 c 0,31,32
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1157
 765 129 765 129 833 217.5 c 128,-1,33
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1158
 901 306 901 306 901 479 c 0,34,35
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1159
 901 653 901 653 833 741 c 128,-1,36
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1160
 765 829 765 829 631 829 c 0,25,26
29073
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1161
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1162
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1163
StartChar: seven
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1164
Encoding: 55 55 26
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1165
Width: 1233
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1166
Flags: W
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1167
TtfInstrs: 53
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1168
5T'_O!WrK+,m4AS63W\UL][e_!<`EI!$;FWr9V?63B8eo0D+Tb92ept&-_G+&-_H(+ohTC
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1169
EndTtf
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1170
Fore
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1171
139 1493 m 1,0,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1172
 1079 1493 l 1,1,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1173
 1079 1407 l 1,2,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1174
 545 0 l 1,3,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1175
 334 0 l 1,4,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1176
 854 1323 l 1,5,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1177
 139 1323 l 1,6,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1178
 139 1493 l 1,0,-1
29073
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1179
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1180
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1181
StartChar: eight
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1182
Encoding: 56 56 27
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1183
Width: 1233
29085
29de5c277f2a replaced single quote by mathematical prime;
wenzelm
parents: 29082
diff changeset
  1184
Flags: HW
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1185
TtfInstrs: 67
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1186
5U@6U!1,&;QQ@`F&saT,-`Jd:$m[;D'dOh2#p'g#+p/ks+WiBLr5@t"`9\''&FL,j3ACLFm,[g*
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1187
&FL+t3B8bn
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1188
EndTtf
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1189
Fore
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1190
616 709 m 0,0,1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1191
 481 709 481 709 407.5 633.5 c 128,-1,2
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1192
 334 558 334 558 334 420 c 256,3,4
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1193
 334 282 334 282 408.5 205.5 c 128,-1,5
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1194
 483 129 483 129 616 129 c 0,6,7
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1195
 752 129 752 129 825.5 204.5 c 128,-1,8
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1196
 899 280 899 280 899 420 c 0,9,10
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1197
 899 557 899 557 824.5 633 c 128,-1,11
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1198
 750 709 750 709 616 709 c 0,0,1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1199
440 793 m 1,12,13
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1200
 311 826 311 826 238.5 916 c 128,-1,14
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1201
 166 1006 166 1006 166 1133 c 0,15,16
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1202
 166 1311 166 1311 287 1415.5 c 128,-1,17
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1203
 408 1520 408 1520 616 1520 c 0,18,19
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1204
 825 1520 825 1520 946 1415.5 c 128,-1,20
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1205
 1067 1311 1067 1311 1067 1133 c 0,21,22
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1206
 1067 1006 1067 1006 994.5 916 c 128,-1,23
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1207
 922 826 922 826 793 793 c 1,24,25
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1208
 943 760 943 760 1022.5 660 c 128,-1,26
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1209
 1102 560 1102 560 1102 401 c 0,27,28
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1210
 1102 199 1102 199 973 85 c 128,-1,29
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1211
 844 -29 844 -29 616 -29 c 256,30,31
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1212
 388 -29 388 -29 259.5 84.5 c 128,-1,32
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1213
 131 198 131 198 131 399 c 0,33,34
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1214
 131 559 131 559 210.5 659.5 c 128,-1,35
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1215
 290 760 290 760 440 793 c 1,12,13
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1216
367 1114 m 0,36,37
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1217
 367 994 367 994 431 931 c 128,-1,38
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1218
 495 868 495 868 616 868 c 0,39,40
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1219
 738 868 738 868 802 931 c 128,-1,41
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1220
 866 994 866 994 866 1114 c 0,42,43
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1221
 866 1236 866 1236 802.5 1300 c 128,-1,44
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1222
 739 1364 739 1364 616 1364 c 0,45,46
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1223
 495 1364 495 1364 431 1299.5 c 128,-1,47
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1224
 367 1235 367 1235 367 1114 c 0,36,37
29073
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1225
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1226
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1227
StartChar: nine
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1228
Encoding: 57 57 28
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1229
Width: 1233
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1230
Flags: W
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1231
TtfInstrs: 59
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1232
5U$jG!1+J%&.OO+NY%O$#+$<q,+0_j"p4lJ+pf;!-5dmO&H(VUr9Wc)!"e5`lk&UYmL]'Z&NMNF
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1233
EndTtf
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1234
Fore
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1235
596 662 m 0,0,1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1236
 725 662 725 662 798.5 755 c 128,-1,2
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1237
 872 848 872 848 872 1012 c 256,3,4
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1238
 872 1176 872 1176 798.5 1269 c 128,-1,5
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1239
 725 1362 725 1362 596 1362 c 0,6,7
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1240
 462 1362 462 1362 394 1273.5 c 128,-1,8
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1241
 326 1185 326 1185 326 1012 c 0,9,10
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1242
 326 838 326 838 393.5 750 c 128,-1,11
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1243
 461 662 461 662 596 662 c 0,0,1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1244
236 31 m 1,12,-1
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1245
 236 217 l 1,13,14
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1246
 299 180 299 180 370 160.5 c 128,-1,15
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1247
 441 141 441 141 518 141 c 0,16,17
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1248
 710 141 710 141 808.5 285.5 c 128,-1,18
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1249
 907 430 907 430 907 711 c 1,19,20
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1250
 860 611 860 611 775 557.5 c 128,-1,21
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1251
 690 504 690 504 580 504 c 0,22,23
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1252
 364 504 364 504 245.5 637 c 128,-1,24
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1253
 127 770 127 770 127 1014 c 0,25,26
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1254
 127 1255 127 1255 248.5 1387.5 c 128,-1,27
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1255
 370 1520 370 1520 592 1520 c 0,28,29
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1256
 852 1520 852 1520 973 1333 c 128,-1,30
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1257
 1094 1146 1094 1146 1094 745 c 0,31,32
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1258
 1094 368 1094 368 948.5 169.5 c 128,-1,33
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1259
 803 -29 803 -29 526 -29 c 0,34,35
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1260
 453 -29 453 -29 379 -13.5 c 128,-1,36
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1261
 305 2 305 2 236 31 c 1,12,-1
29073
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1262
EndSplineSet
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1263
EndChar
feb740b8c043 Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
wenzelm
parents:
diff changeset
  1264
StartChar: colon
29074
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1265
Encoding: 58 58 29
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1266
Width: 614
7250cd050f3f the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
wenzelm
parents: 29073
diff changeset
  1267
VWidth: 2220