--- a/Admin/isabelle_fonts/IsabelleSymbolsBold.sfd Mon Mar 22 10:49:51 2021 +0000
+++ b/Admin/isabelle_fonts/IsabelleSymbolsBold.sfd Mon Mar 22 17:24:42 2021 +0100
@@ -21,7 +21,7 @@
OS2_WeightWidthSlopeOnly: 0
OS2_UseTypoMetrics: 1
CreationTime: 1050374980
-ModificationTime: 1616363616
+ModificationTime: 1616429477
PfmFamily: 17
TTFWeight: 700
TTFWidth: 5
@@ -1679,10 +1679,10 @@
DisplaySize: -96
AntiAlias: 1
FitToEm: 1
-WinInfo: 8448 11 8
+WinInfo: 10978 11 8
BeginPrivate: 0
EndPrivate
-BeginChars: 1114115 1446
+BeginChars: 1114115 1450
StartChar: .notdef
Encoding: 1114112 -1 0
@@ -70332,43 +70332,44 @@
StartChar: uni2AF4
Encoding: 10996 10996 1424
Width: 1422
-Flags: W
-LayerCount: 2
-Fore
-SplineSet
-1201 -205 m 2,0,1
- 1201 -243 1201 -243 1173.5 -268 c 0,2,3
- 1146 -293 1146 -293 1109 -293 c 0,4,5
- 1072 -293 1072 -293 1044.5 -268.5 c 0,6,7
- 1017 -244 1017 -244 1017 -205 c 2,8,-1
- 1017 1369 l 2,9,10
- 1017 1407 1017 1407 1044.5 1432 c 0,11,12
- 1072 1457 1072 1457 1109 1457 c 0,13,14
- 1146 1457 1146 1457 1173.5 1432.5 c 0,15,16
- 1201 1408 1201 1408 1201 1369 c 2,17,-1
- 1201 -205 l 2,0,1
-803 -205 m 2,18,19
- 803 -243 803 -243 775.5 -268 c 0,20,21
- 748 -293 748 -293 711 -293 c 0,22,23
- 674 -293 674 -293 646.5 -268.5 c 0,24,25
- 619 -244 619 -244 619 -205 c 2,26,-1
- 619 1369 l 2,27,28
- 619 1407 619 1407 646.5 1432 c 0,29,30
- 674 1457 674 1457 711 1457 c 0,31,32
- 748 1457 748 1457 775.5 1432.5 c 0,33,34
- 803 1408 803 1408 803 1369 c 2,35,-1
- 803 -205 l 2,18,19
-405 -205 m 2,36,37
- 405 -243 405 -243 377.5 -268 c 0,38,39
- 350 -293 350 -293 313 -293 c 0,40,41
- 276 -293 276 -293 248.5 -268.5 c 0,42,43
- 221 -244 221 -244 221 -205 c 2,44,-1
- 221 1369 l 2,45,46
- 221 1407 221 1407 248.5 1432 c 0,47,48
- 276 1457 276 1457 313 1457 c 0,49,50
- 350 1457 350 1457 377.5 1432.5 c 0,51,52
- 405 1408 405 1408 405 1369 c 2,53,-1
- 405 -205 l 2,36,37
+VWidth: 2121
+Flags: W
+LayerCount: 2
+Fore
+SplineSet
+1201 -454.349609375 m 2,0,1
+ 1201 -501.261464692 1201 -501.261464692 1168.11312524 -526.191695994 c 0,2,3
+ 1144.35709768 -544.200195312 1144.35709768 -544.200195312 1109 -544.200195312 c 0,4,5
+ 1073.64290232 -544.200195312 1073.64290232 -544.200195312 1049.88687476 -526.191695994 c 0,6,7
+ 1017 -501.261464692 1017 -501.261464692 1017 -454.349609375 c 2,8,-1
+ 1017 1618.34960938 l 2,9,10
+ 1017 1665.26146469 1017 1665.26146469 1049.88687476 1690.19169599 c 0,11,12
+ 1073.64290232 1708.20019531 1073.64290232 1708.20019531 1109 1708.20019531 c 0,13,14
+ 1144.35709768 1708.20019531 1144.35709768 1708.20019531 1168.11312524 1690.19169599 c 0,15,16
+ 1201 1665.26146469 1201 1665.26146469 1201 1618.34960938 c 2,17,-1
+ 1201 -454.349609375 l 2,0,1
+803 -454.349609375 m 2,18,19
+ 803 -501.261464692 803 -501.261464692 770.113125236 -526.191695994 c 0,20,21
+ 746.357097681 -544.200195312 746.357097681 -544.200195312 711 -544.200195312 c 0,22,23
+ 675.642902319 -544.200195312 675.642902319 -544.200195312 651.886874764 -526.191695994 c 0,24,25
+ 619 -501.261464692 619 -501.261464692 619 -454.349609375 c 2,26,-1
+ 619 1618.34960938 l 2,27,28
+ 619 1665.26146469 619 1665.26146469 651.886874764 1690.19169599 c 0,29,30
+ 675.642902319 1708.20019531 675.642902319 1708.20019531 711 1708.20019531 c 0,31,32
+ 746.357097681 1708.20019531 746.357097681 1708.20019531 770.113125236 1690.19169599 c 0,33,34
+ 803 1665.26146469 803 1665.26146469 803 1618.34960938 c 2,35,-1
+ 803 -454.349609375 l 2,18,19
+405 -454.349609375 m 2,36,37
+ 405 -501.261464692 405 -501.261464692 372.113125236 -526.191695994 c 0,38,39
+ 348.357097681 -544.200195312 348.357097681 -544.200195312 313 -544.200195312 c 0,40,41
+ 277.642902319 -544.200195312 277.642902319 -544.200195312 253.886874764 -526.191695994 c 0,42,43
+ 221 -501.261464692 221 -501.261464692 221 -454.349609375 c 2,44,-1
+ 221 1618.34960938 l 2,45,46
+ 221 1665.26146469 221 1665.26146469 253.886874764 1690.19169599 c 0,47,48
+ 277.642902319 1708.20019531 277.642902319 1708.20019531 313 1708.20019531 c 0,49,50
+ 348.357097681 1708.20019531 348.357097681 1708.20019531 372.113125236 1690.19169599 c 0,51,52
+ 405 1665.26146469 405 1665.26146469 405 1618.34960938 c 2,53,-1
+ 405 -454.349609375 l 2,36,37
EndSplineSet
EndChar
@@ -71526,5 +71527,215 @@
469.73046875 175.900390625 469.73046875 175.900390625 469.73046875 273.580078125 c 2,44,-1
EndSplineSet
EndChar
+
+StartChar: uni2AFB
+Encoding: 11003 11003 1446
+Width: 1625
+Flags: W
+LayerCount: 2
+Fore
+SplineSet
+1586.40527344 1601.80566406 m 0,0,1
+ 1592 1586.36621094 1592 1586.36621094 1592 1572.52441406 c 128,-1,2
+ 1592 1558.68261719 1592 1558.68261719 1589.47070312 1546.58886719 c 128,-1,3
+ 1586.94140625 1534.49511719 1586.94140625 1534.49511719 1581.87304688 1517.38964844 c 2,4,-1
+ 1005.88671875 -409.563476562 l 2,5,6
+ 990.52734375 -461.126953125 990.52734375 -461.126953125 956.502929688 -481.37890625 c 0,7,8
+ 936.98046875 -493 936.98046875 -493 914 -493 c 0,9,10
+ 878.822265625 -493 878.822265625 -493 855.10546875 -475.833984375 c 0,11,12
+ 835.138671875 -461.380859375 835.138671875 -461.380859375 826.594726562 -437.805664062 c 0,13,14
+ 821 -422.366210938 821 -422.366210938 821 -408.524414062 c 128,-1,15
+ 821 -394.682617188 821 -394.682617188 823.529296875 -382.588867188 c 128,-1,16
+ 826.05859375 -370.495117188 826.05859375 -370.495117188 831.126953125 -353.389648438 c 2,17,-1
+ 1407.11328125 1573.56347656 l 2,18,19
+ 1422.47265625 1625.12695312 1422.47265625 1625.12695312 1456.49707031 1645.37890625 c 0,20,21
+ 1476.01953125 1657 1476.01953125 1657 1499 1657 c 0,22,23
+ 1534.17773438 1657 1534.17773438 1657 1557.89453125 1639.83398438 c 0,24,25
+ 1577.86132812 1625.38085938 1577.86132812 1625.38085938 1586.40527344 1601.80566406 c 0,0,1
+1186.40527344 1601.80566406 m 0,26,27
+ 1192 1586.36621094 1192 1586.36621094 1192 1572.52441406 c 128,-1,28
+ 1192 1558.68261719 1192 1558.68261719 1189.47070312 1546.58886719 c 128,-1,29
+ 1186.94140625 1534.49511719 1186.94140625 1534.49511719 1181.87304688 1517.38964844 c 2,30,-1
+ 605.88671875 -409.563476562 l 2,31,32
+ 590.52734375 -461.126953125 590.52734375 -461.126953125 556.502929688 -481.37890625 c 0,33,34
+ 536.98046875 -493 536.98046875 -493 514 -493 c 0,35,36
+ 478.822265625 -493 478.822265625 -493 455.10546875 -475.833984375 c 0,37,38
+ 435.138671875 -461.380859375 435.138671875 -461.380859375 426.594726562 -437.805664062 c 0,39,40
+ 421 -422.366210938 421 -422.366210938 421 -408.524414062 c 128,-1,41
+ 421 -394.682617188 421 -394.682617188 423.529296875 -382.588867188 c 128,-1,42
+ 426.05859375 -370.495117188 426.05859375 -370.495117188 431.126953125 -353.389648438 c 2,43,-1
+ 1007.11328125 1573.56347656 l 2,44,45
+ 1022.47265625 1625.12695312 1022.47265625 1625.12695312 1056.49707031 1645.37890625 c 0,46,47
+ 1076.01953125 1657 1076.01953125 1657 1099 1657 c 0,48,49
+ 1134.17773438 1657 1134.17773438 1657 1157.89453125 1639.83398438 c 0,50,51
+ 1177.86132812 1625.38085938 1177.86132812 1625.38085938 1186.40527344 1601.80566406 c 0,26,27
+786.405273438 1601.80566406 m 0,52,53
+ 792 1586.36621094 792 1586.36621094 792 1572.52441406 c 128,-1,54
+ 792 1558.68261719 792 1558.68261719 789.470703125 1546.58886719 c 128,-1,55
+ 786.94140625 1534.49511719 786.94140625 1534.49511719 781.873046875 1517.38964844 c 2,56,-1
+ 205.88671875 -409.563476562 l 2,57,58
+ 190.52734375 -461.126953125 190.52734375 -461.126953125 156.502929688 -481.37890625 c 0,59,60
+ 136.98046875 -493 136.98046875 -493 114 -493 c 0,61,62
+ 78.822265625 -493 78.822265625 -493 55.10546875 -475.833984375 c 0,63,64
+ 35.138671875 -461.380859375 35.138671875 -461.380859375 26.5947265625 -437.805664062 c 0,65,66
+ 21 -422.366210938 21 -422.366210938 21 -408.524414062 c 128,-1,67
+ 21 -394.682617188 21 -394.682617188 23.529296875 -382.588867188 c 128,-1,68
+ 26.05859375 -370.495117188 26.05859375 -370.495117188 31.126953125 -353.389648438 c 2,69,-1
+ 607.11328125 1573.56347656 l 2,70,71
+ 622.47265625 1625.12695312 622.47265625 1625.12695312 656.497070312 1645.37890625 c 0,72,73
+ 676.01953125 1657 676.01953125 1657 699 1657 c 0,74,75
+ 734.177734375 1657 734.177734375 1657 757.89453125 1639.83398438 c 0,76,77
+ 777.861328125 1625.38085938 777.861328125 1625.38085938 786.405273438 1601.80566406 c 0,52,53
+EndSplineSet
+EndChar
+
+StartChar: uni2AFD
+Encoding: 11005 11005 1447
+Width: 1245
+Flags: W
+LayerCount: 2
+Fore
+SplineSet
+1194.40527344 1601.80566406 m 0,0,1
+ 1200 1586.36621094 1200 1586.36621094 1200 1572.52441406 c 128,-1,2
+ 1200 1558.68261719 1200 1558.68261719 1197.47070312 1546.58886719 c 128,-1,3
+ 1194.94140625 1534.49511719 1194.94140625 1534.49511719 1189.87304688 1517.38964844 c 2,4,-1
+ 613.88671875 -409.563476562 l 2,5,6
+ 598.52734375 -461.126953125 598.52734375 -461.126953125 564.502929688 -481.37890625 c 0,7,8
+ 544.98046875 -493 544.98046875 -493 522 -493 c 0,9,10
+ 486.822265625 -493 486.822265625 -493 463.10546875 -475.833984375 c 0,11,12
+ 443.138671875 -461.380859375 443.138671875 -461.380859375 434.594726562 -437.805664062 c 0,13,14
+ 429 -422.366210938 429 -422.366210938 429 -408.524414062 c 128,-1,15
+ 429 -394.682617188 429 -394.682617188 431.529296875 -382.588867188 c 128,-1,16
+ 434.05859375 -370.495117188 434.05859375 -370.495117188 439.126953125 -353.389648438 c 2,17,-1
+ 1015.11328125 1573.56347656 l 2,18,19
+ 1030.47265625 1625.12695312 1030.47265625 1625.12695312 1064.49707031 1645.37890625 c 0,20,21
+ 1084.01953125 1657 1084.01953125 1657 1107 1657 c 0,22,23
+ 1142.17773438 1657 1142.17773438 1657 1165.89453125 1639.83398438 c 0,24,25
+ 1185.86132812 1625.38085938 1185.86132812 1625.38085938 1194.40527344 1601.80566406 c 0,0,1
+794.405273438 1601.80566406 m 0,26,27
+ 800 1586.36621094 800 1586.36621094 800 1572.52441406 c 128,-1,28
+ 800 1558.68261719 800 1558.68261719 797.470703125 1546.58886719 c 128,-1,29
+ 794.94140625 1534.49511719 794.94140625 1534.49511719 789.873046875 1517.38964844 c 2,30,-1
+ 213.88671875 -409.563476562 l 2,31,32
+ 198.52734375 -461.126953125 198.52734375 -461.126953125 164.502929688 -481.37890625 c 0,33,34
+ 144.98046875 -493 144.98046875 -493 122 -493 c 0,35,36
+ 86.822265625 -493 86.822265625 -493 63.10546875 -475.833984375 c 0,37,38
+ 43.138671875 -461.380859375 43.138671875 -461.380859375 34.5947265625 -437.805664062 c 0,39,40
+ 29 -422.366210938 29 -422.366210938 29 -408.524414062 c 128,-1,41
+ 29 -394.682617188 29 -394.682617188 31.529296875 -382.588867188 c 128,-1,42
+ 34.05859375 -370.495117188 34.05859375 -370.495117188 39.126953125 -353.389648438 c 2,43,-1
+ 615.11328125 1573.56347656 l 2,44,45
+ 630.47265625 1625.12695312 630.47265625 1625.12695312 664.497070312 1645.37890625 c 0,46,47
+ 684.01953125 1657 684.01953125 1657 707 1657 c 0,48,49
+ 742.177734375 1657 742.177734375 1657 765.89453125 1639.83398438 c 0,50,51
+ 785.861328125 1625.38085938 785.861328125 1625.38085938 794.405273438 1601.80566406 c 0,26,27
+EndSplineSet
+EndChar
+
+StartChar: uni2713
+Encoding: 10003 10003 1448
+Width: 1607
+Flags: W
+LayerCount: 2
+Fore
+SplineSet
+1493 1495 m 2,0,-1
+ 1526.77164471 1495 l 1,1,-1
+ 1566.19736724 1402.06793975 l 1,2,-1
+ 1356.86511893 1154.1744878 l 1,3,-1
+ 932.845222843 593.791385703 l 1,4,-1
+ 639.483803336 139.329796839 l 1,5,-1
+ 568.818379563 18.6096978939 l 1,6,7
+ 554.602777558 -9.06411668208 554.602777558 -9.06411668208 518.644035855 -48.3939904199 c 2,8,-1
+ 511.711411812 -55.9765479671 l 1,9,-1
+ 502.43244588 -60.2846392926 l 2,10,11
+ 464.276284356 -78 464.276284356 -78 364 -78 c 0,12,13
+ 296.068423746 -78 296.068423746 -78 268.932432206 -71.4123643321 c 0,14,15
+ 257.09240277 -68.5380341235 257.09240277 -68.5380341235 247.832464497 -63.4391645962 c 0,16,17
+ 230.142067601 -53.6981681654 230.142067601 -53.6981681654 214.007699323 -30.1527981905 c 0,18,19
+ 197.873331045 -6.60742821566 197.873331045 -6.60742821566 179.040881649 32.8799656793 c 0,20,21
+ 49 302.324672457 49 302.324672457 49 457 c 0,22,23
+ 49 519.501521162 49 519.501521162 117.742185968 567.76731131 c 0,24,25
+ 175.199891064 608.109955313 175.199891064 608.109955313 221.191313606 625.554977657 c 0,26,27
+ 267.182736147 643 267.182736147 643 305 643 c 0,28,29
+ 328.250160553 643 328.250160553 643 347.696288159 633.597476762 c 0,30,31
+ 372.843130313 621.438564072 372.843130313 621.438564072 387.939724284 595.890481966 c 2,32,-1
+ 390.023978812 592.363281996 l 1,33,-1
+ 409.230482467 543.279994878 l 1,34,35
+ 451.928255863 443.303347135 451.928255863 443.303347135 455.092353441 436.318212809 c 1,36,37
+ 458.200659317 440.782578532 458.200659317 440.782578532 935.97326392 1148.36985379 c 1,38,-1
+ 1102.42124961 1353.15130657 l 2,39,40
+ 1160.87193959 1424.99694635 1160.87193959 1424.99694635 1287.24905492 1463.83062241 c 0,41,42
+ 1390.43044278 1495 1390.43044278 1495 1493 1495 c 2,0,-1
+EndSplineSet
+EndChar
+
+StartChar: uni2717
+Encoding: 10007 10007 1449
+Width: 1371
+Flags: W
+LayerCount: 2
+Fore
+SplineSet
+1167.81653987 1380.08960467 m 1,0,1
+ 1190.53865647 1405 1190.53865647 1405 1218 1405 c 0,2,3
+ 1233.56059461 1405 1233.56059461 1405 1244.79021364 1398.01039731 c 0,4,5
+ 1256.01983266 1391.02079462 1256.01983266 1391.02079462 1263.23081059 1381.76897388 c 0,6,7
+ 1270.44178852 1372.51715315 1270.44178852 1372.51715315 1276.09560061 1359.00435305 c 0,8,9
+ 1281.19707005 1351.91701104 1281.19707005 1351.91701104 1292.75684028 1339.43347912 c 0,10,11
+ 1312.53847517 1318.07105878 1312.53847517 1318.07105878 1318.68504378 1299.81213438 c 0,12,13
+ 1322 1289.96476444 1322 1289.96476444 1322 1280 c 0,14,15
+ 1322 1260.31858868 1322 1260.31858868 1311.64031985 1243.3663848 c 0,16,17
+ 1301.2806397 1226.41418092 1301.2806397 1226.41418092 1285.09495619 1211.04044106 c 0,18,19
+ 1268.90927267 1195.6667012 1268.90927267 1195.6667012 1219.41730343 1131.90710342 c 2,20,-1
+ 925.797183091 748.230971729 l 1,21,-1
+ 974.975591014 649.093546232 l 1,22,-1
+ 1144.88520065 285.91175563 l 1,23,-1
+ 1135.90032198 264.947038723 l 2,24,25
+ 1127.38194848 245.0708339 1127.38194848 245.0708339 1112 229.962486833 c 1,26,-1
+ 1112 218.88925125 l 1,27,-1
+ 1097.05537437 203.944625625 l 2,28,29
+ 1092.34173643 199.23098768 1092.34173643 199.23098768 1080.19057178 191.668254725 c 1,30,-1
+ 1083.03885777 185.971682746 l 1,31,-1
+ 1080.30488745 169.567860837 l 2,32,33
+ 1073.85215579 130.851470867 1073.85215579 130.851470867 1033.68158842 102.033455151 c 0,34,35
+ 997.392529728 76 997.392529728 76 962 76 c 0,36,37
+ 943.007224586 76 943.007224586 76 924.98549081 87.6477992087 c 0,38,39
+ 912.740176189 95.5621856784 912.740176189 95.5621856784 899.221613263 110.220868369 c 0,40,41
+ 875.720605027 135.703889348 875.720605027 135.703889348 841.13897792 189.365034859 c 2,42,-1
+ 692.033039 420.013284126 l 1,43,-1
+ 323.904736667 -150.313568503 l 1,44,-1
+ 316.557164915 -155.824247317 l 2,45,46
+ 270.989494671 -190 270.989494671 -190 180 -190 c 0,47,48
+ 153.415988707 -190 153.415988707 -190 129.712547601 -169.431934702 c 0,49,50
+ 112.364223766 -154.378362697 112.364223766 -154.378362697 93.6332162638 -124.805706407 c 0,51,52
+ 65.1809628297 -79.8850735255 65.1809628297 -79.8850735255 58.2559561219 -56.2339417453 c 0,53,54
+ 55 -45.1138012807 55 -45.1138012807 55 -31.1783142002 c 0,55,56
+ 55 -17.2428271197 55 -17.2428271197 63.517843618 14.0152361593 c 1,57,58
+ 49 32.5566876995 49 32.5566876995 49 53 c 0,59,60
+ 49 71.8596649377 49 71.8596649377 62.7535430459 101.401714031 c 0,61,62
+ 76.5070860918 130.943763125 76.5070860918 130.943763125 104.914813556 179.642724493 c 2,63,-1
+ 153.950326996 263.70350823 l 2,64,65
+ 235.710604342 403.420437872 235.710604342 403.420437872 515.13212247 741.054772277 c 1,66,-1
+ 373.988921799 1131.76925335 l 2,67,68
+ 354.758358862 1185.280385 354.758358862 1185.280385 352.16040039 1195.26275804 c 0,69,70
+ 348 1211.24864432 348 1211.24864432 348 1220.73772757 c 0,71,72
+ 348 1237.05889048 348 1237.05889048 360.504822959 1258.01604748 c 0,73,74
+ 368.91805291 1272.11599767 368.91805291 1272.11599767 389.101026052 1297.53159348 c 1,75,-1
+ 406.837383245 1312.73418536 l 2,76,77
+ 428.147500321 1331 428.147500321 1331 454 1331 c 0,78,79
+ 472.642818219 1331 472.642818219 1331 492.73394757 1319.97607702 c 0,80,81
+ 496.545848238 1320.87009822 496.545848238 1320.87009822 500.504324991 1321.5010432 c 0,82,83
+ 525.1114794 1353.99999987 525.1114794 1353.99999987 561 1354 c 0,84,85
+ 611.824626312 1354 611.824626312 1354 643.733999519 1288.58292127 c 2,86,-1
+ 763.130059127 1051.33139637 l 1,87,-1
+ 866.508498698 1170.44368469 l 2,88,89
+ 1018.07235609 1344.7015956 1018.07235609 1344.7015956 1055.15990561 1380.36868264 c 0,90,91
+ 1067.39695571 1392.13705065 1067.39695571 1392.13705065 1074.12207933 1395.67520223 c 0,92,93
+ 1088.04465143 1403 1088.04465143 1403 1101 1403 c 0,94,95
+ 1131.20656165 1403 1131.20656165 1403 1167.81653987 1380.08960467 c 1,0,1
+EndSplineSet
+EndChar
EndChars
EndSplineFont