--- a/Admin/isabelle_fonts/IsabelleSymbolsBold.sfd Wed Jul 17 11:18:39 2019 +0200
+++ b/Admin/isabelle_fonts/IsabelleSymbolsBold.sfd Wed Jul 17 16:10:05 2019 +0200
@@ -21,7 +21,7 @@
OS2_WeightWidthSlopeOnly: 0
OS2_UseTypoMetrics: 1
CreationTime: 1050374980
-ModificationTime: 1563354308
+ModificationTime: 1563372497
PfmFamily: 17
TTFWeight: 700
TTFWidth: 5
@@ -1679,10 +1679,10 @@
DisplaySize: -96
AntiAlias: 1
FitToEm: 1
-WinInfo: 10944 32 8
+WinInfo: 10176 32 8
BeginPrivate: 0
EndPrivate
-BeginChars: 1114115 1404
+BeginChars: 1114115 1406
StartChar: .notdef
Encoding: 1114112 -1 0
@@ -69163,24 +69163,185 @@
LayerCount: 2
Fore
SplineSet
-401 1525 m 1
- 401 -415 l 1
- 737 -415 l 1
- 737 1525 l 1
- 401 1525 l 1
-264 1721 m 1
- 880 1721 l 1
- 931 1721 l 1
- 931 1670 l 1
- 931 -558 l 1
- 931 -609 l 1
- 880 -609 l 1
- 264 -609 l 1
- 213 -609 l 1
- 213 -558 l 1
- 213 1670 l 1
- 213 1721 l 1
- 264 1721 l 1
+401 1525 m 1,0,-1
+ 401 -415 l 1,1,-1
+ 737 -415 l 1,2,-1
+ 737 1525 l 1,3,-1
+ 401 1525 l 1,0,-1
+264 1721 m 1,4,-1
+ 880 1721 l 1,5,-1
+ 931 1721 l 1,6,-1
+ 931 1670 l 1,7,-1
+ 931 -558 l 1,8,-1
+ 931 -609 l 1,9,-1
+ 880 -609 l 1,10,-1
+ 264 -609 l 1,11,-1
+ 213 -609 l 1,12,-1
+ 213 -558 l 1,13,-1
+ 213 1670 l 1,14,-1
+ 213 1721 l 1,15,-1
+ 264 1721 l 1,4,-1
+EndSplineSet
+EndChar
+
+StartChar: uni27EA
+Encoding: 10218 10218 1404
+Width: 1161
+VWidth: 2220
+Flags: W
+LayerCount: 2
+Fore
+SplineSet
+773.433067855 1562.25171141 m 2
+ 389.577883489 555 l 1
+ 773.433067855 -452.251711406 l 2
+ 781.390968826 -472.014126234 781.390968826 -472.014126234 784.695484413 -483.995108037 c 0
+ 788 -495.97608984 788 -495.97608984 788 -511 c 0
+ 788 -550.124891681 788 -550.124891681 760.062445841 -578.062445841 c 0
+ 732.124891681 -606 732.124891681 -606 693 -606 c 0
+ 690.966017759 -606 690.966017759 -606 688.963489691 -605.928643068 c 0
+ 686.960961624 -605.857286137 686.960961624 -605.857286137 684.892393771 -605.709011758 c 0
+ 682.823825917 -605.560737379 682.823825917 -605.560737379 680.76747727 -605.324534758 c 0
+ 678.711128623 -605.088332136 678.711128623 -605.088332136 676.625730612 -604.767155106 c 0
+ 674.540332601 -604.445978076 674.540332601 -604.445978076 672.44417047 -604.01973387 c 0
+ 670.348008338 -603.593489663 670.348008338 -603.593489663 668.259787265 -603.074214086 c 0
+ 666.171566192 -602.554938509 666.171566192 -602.554938509 664.049597672 -601.913456822 c 0
+ 661.927629152 -601.271975134 661.927629152 -601.271975134 659.846843753 -600.528837491 c 0
+ 654.406114092 -598.585719755 654.406114092 -598.585719755 649.309616546 -595.97667424 c 0
+ 644.213119 -593.367628724 644.213119 -593.367628724 639.0284107 -589.668111402 c 0
+ 633.8437024 -585.968594081 633.8437024 -585.968594081 629.437554159 -581.562445841 c 0
+ 621.366668313 -573.491559994 621.366668313 -573.491559994 614.565434989 -563.289710007 c 0
+ 611.010645977 -557.95752649 611.010645977 -557.95752649 608.043624405 -552.235368077 c 0
+ 605.076602833 -546.513209663 605.076602833 -546.513209663 602.647688765 -540.440924494 c 0
+ 601.07426099 -536.507355058 601.07426099 -536.507355058 599.445196471 -532.299218632 c 0
+ 597.816131951 -528.091082206 597.816131951 -528.091082206 596.294209878 -524.032623346 c 2
+ 207.565919702 496.254225678 l 2
+ 199.609686199 516.012499566 199.609686199 516.012499566 196.304843099 527.994862915 c 0
+ 193 539.977226263 193 539.977226263 193 555 c 0
+ 193 565.225713049 193 565.225713049 195.245324552 576.018756482 c 0
+ 197.490649104 586.811799915 197.490649104 586.811799915 200.081716986 594.203054286 c 0
+ 202.672784867 601.594308656 202.672784867 601.594308656 207.566932145 613.748288594 c 2
+ 597.972039167 1638.18726508 l 2
+ 600.194483765 1644.75231063 600.194483765 1644.75231063 601.986957781 1649.47802294 c 0
+ 603.779431796 1654.20373526 603.779431796 1654.20373526 606.068369421 1659.21033763 c 0
+ 608.357307047 1664.21694 608.357307047 1664.21694 611.049647607 1669.00332322 c 0
+ 621.382343055 1687.37255957 621.382343055 1687.37255957 640.701120305 1700.59067032 c 0
+ 663.222448293 1716 663.222448293 1716 693 1716 c 0
+ 700.423944801 1716 700.423944801 1716 707.872943823 1714.76786733 c 0
+ 715.321942844 1713.53573466 715.321942844 1713.53573466 722.391875006 1711.16829501 c 0
+ 729.461807167 1708.80085536 729.461807167 1708.80085536 736.118390492 1705.41106402 c 0
+ 742.774973817 1702.02127269 742.774973817 1702.02127269 748.821381789 1697.6391873 c 0
+ 754.867789762 1693.25710192 754.867789762 1693.25710192 760.062445841 1688.06244584 c 0
+ 768.737564682 1679.387327 768.737564682 1679.387327 775.010481308 1668.56083179 c 0
+ 781.283397934 1657.73433659 781.283397934 1657.73433659 784.641698967 1645.54589151 c 0
+ 788 1633.35744643 788 1633.35744643 788 1621 c 0
+ 788 1610.77428695 788 1610.77428695 785.754675448 1599.98124352 c 0
+ 783.509350896 1589.18820008 783.509350896 1589.18820008 780.918283014 1581.79694571 c 0
+ 778.327215133 1574.40569134 778.327215133 1574.40569134 773.433067855 1562.25171141 c 2
+1073.43306785 1562.25171141 m 2
+ 689.577883489 555 l 1
+ 1073.43306785 -452.251711406 l 2
+ 1088 -488.426797886 1088 -488.426797886 1088 -511 c 0
+ 1088 -518.423944801 1088 -518.423944801 1086.76786733 -525.872943823 c 0
+ 1085.53573466 -533.321942844 1085.53573466 -533.321942844 1083.16829501 -540.391875006 c 0
+ 1080.80085536 -547.461807167 1080.80085536 -547.461807167 1077.41106402 -554.118390492 c 0
+ 1074.02127269 -560.774973817 1074.02127269 -560.774973817 1069.6391873 -566.821381789 c 0
+ 1065.25710192 -572.867789762 1065.25710192 -572.867789762 1060.06244584 -578.062445841 c 0
+ 1046.94472562 -591.180166062 1046.94472562 -591.180166062 1029.27411163 -598.590083031 c 0
+ 1011.60349764 -606 1011.60349764 -606 993 -606 c 0
+ 984.51752108 -606 984.51752108 -606 976.206536445 -604.701688042 c 0
+ 967.895551811 -603.403376083 967.895551811 -603.403376083 959.846843753 -600.528837491 c 0
+ 954.406114092 -598.585719755 954.406114092 -598.585719755 949.309616546 -595.97667424 c 0
+ 944.213119 -593.367628724 944.213119 -593.367628724 939.0284107 -589.668111402 c 0
+ 933.8437024 -585.968594081 933.8437024 -585.968594081 929.437554159 -581.562445841 c 0
+ 921.366668313 -573.491559994 921.366668313 -573.491559994 914.565434989 -563.289710007 c 0
+ 911.010645977 -557.95752649 911.010645977 -557.95752649 908.043624405 -552.235368077 c 0
+ 905.076602833 -546.513209663 905.076602833 -546.513209663 902.647688765 -540.440924494 c 0
+ 901.07426099 -536.507355058 901.07426099 -536.507355058 899.445196471 -532.299218632 c 0
+ 897.816131951 -528.091082206 897.816131951 -528.091082206 896.294209878 -524.032623346 c 2
+ 507.565919702 496.254225678 l 2
+ 499.609686199 516.012499566 499.609686199 516.012499566 496.304843099 527.994862915 c 0
+ 493 539.977226263 493 539.977226263 493 555 c 0
+ 493 562.810879998 493 562.810879998 494.055472434 570.258924161 c 0
+ 495.110944868 577.706968323 495.110944868 577.706968323 497.451348895 585.545645538 c 0
+ 499.791752921 593.384322753 499.791752921 593.384322753 501.859659434 599.04735873 c 0
+ 503.927565946 604.710394707 503.927565946 604.710394707 507.566932145 613.748288594 c 2
+ 897.972039167 1638.18726508 l 2
+ 901.32118185 1648.08054848 901.32118185 1648.08054848 904.224607807 1655.05605688 c 0
+ 907.128033763 1662.03156528 907.128033763 1662.03156528 911.049647607 1669.00332322 c 0
+ 921.382343055 1687.37255957 921.382343055 1687.37255957 940.701120305 1700.59067032 c 0
+ 963.222448293 1716 963.222448293 1716 993 1716 c 0
+ 1000.4239448 1716 1000.4239448 1716 1007.87294382 1714.76786733 c 0
+ 1015.32194284 1713.53573466 1015.32194284 1713.53573466 1022.39187501 1711.16829501 c 0
+ 1029.46180717 1708.80085536 1029.46180717 1708.80085536 1036.11839049 1705.41106402 c 0
+ 1042.77497382 1702.02127269 1042.77497382 1702.02127269 1048.82138179 1697.6391873 c 0
+ 1054.86778976 1693.25710192 1054.86778976 1693.25710192 1060.06244584 1688.06244584 c 0
+ 1073.18016606 1674.94472562 1073.18016606 1674.94472562 1080.59008303 1657.27411163 c 0
+ 1088 1639.60349764 1088 1639.60349764 1088 1621 c 0
+ 1088 1598.42679789 1088 1598.42679789 1073.43306785 1562.25171141 c 2
+EndSplineSet
+EndChar
+
+StartChar: uni27EB
+Encoding: 10219 10219 1405
+Width: 1061
+VWidth: 2220
+Flags: W
+LayerCount: 2
+Fore
+SplineSet
+653.433067855 496.251711406 m 2
+ 262.795873515 -528.796271696 l 2
+ 255.492538225 -548.880443742 255.492538225 -548.880443742 244.246012333 -565.137792244 c 0
+ 232.99948644 -581.395140747 232.99948644 -581.395140747 213.079715784 -593.697570373 c 0
+ 193.159945129 -606 193.159945129 -606 169 -606 c 0
+ 129.875108319 -606 129.875108319 -606 101.437554159 -577.562445841 c 0
+ 73 -549.124891681 73 -549.124891681 73 -511 c 0
+ 73 -488.426797886 73 -488.426797886 87.5669321452 -452.251711406 c 2
+ 471.422116511 555 l 1
+ 87.5669321452 1562.25171141 l 2
+ 73 1598.42679789 73 1598.42679789 73 1621 c 0
+ 73 1633.6040069 73 1633.6040069 76.5609657568 1646.01567027 c 0
+ 80.1219315135 1658.42733364 80.1219315135 1658.42733364 86.6484595992 1669.27291665 c 0
+ 93.1749876849 1680.11849966 93.1749876849 1680.11849966 102.12427396 1688.73633089 c 0
+ 115.390346368 1701.51106728 115.390346368 1701.51106728 132.945757373 1708.75553364 c 0
+ 150.501168378 1716 150.501168378 1716 169 1716 c 0
+ 186.683227377 1716 186.683227377 1716 200.640795179 1712.27798192 c 0
+ 227.920396727 1705.00342151 227.920396727 1705.00342151 245.564126336 1676.01729429 c 0
+ 253.667102023 1662.70526281 253.667102023 1662.70526281 255.615786741 1658.80789337 c 0
+ 257.674333935 1654.69079898 257.674333935 1654.69079898 265.603655969 1634.30111375 c 2
+ 653.444670969 613.719473764 l 2
+ 661.383463777 594.004511582 661.383463777 594.004511582 664.691731888 582.007697863 c 0
+ 668 570.010884144 668 570.010884144 668 555 c 0
+ 668 540.337813677 668 540.337813677 664.406510997 527.45834196 c 0
+ 660.813021994 514.578870243 660.813021994 514.578870243 653.433067855 496.251711406 c 2
+953.433067855 496.251711406 m 2
+ 562.795873515 -528.796271696 l 2
+ 551.145513147 -560.834762708 551.145513147 -560.834762708 527.661549555 -583.417381354 c 0
+ 504.177585963 -606 504.177585963 -606 469 -606 c 0
+ 429.875108319 -606 429.875108319 -606 401.437554159 -577.562445841 c 0
+ 373 -549.124891681 373 -549.124891681 373 -511 c 0
+ 373 -500.774286951 373 -500.774286951 375.245324552 -489.981243518 c 0
+ 377.490649104 -479.188200085 377.490649104 -479.188200085 380.081716986 -471.796945714 c 0
+ 382.672784867 -464.405691344 382.672784867 -464.405691344 387.566932145 -452.251711406 c 2
+ 771.422116511 555 l 1
+ 387.566932145 1562.25171141 l 2
+ 373 1598.42679789 373 1598.42679789 373 1621 c 0
+ 373 1639.9408395 373 1639.9408395 380.780095648 1657.80773058 c 0
+ 388.560191296 1675.67462166 388.560191296 1675.67462166 402.12427396 1688.73633089 c 0
+ 410.883148534 1697.1708027 410.883148534 1697.1708027 421.628761565 1703.27369144 c 0
+ 432.374374596 1709.37658019 432.374374596 1709.37658019 444.529941996 1712.68829009 c 0
+ 456.685509397 1716 456.685509397 1716 469 1716 c 0
+ 486.683227377 1716 486.683227377 1716 500.640795179 1712.27798192 c 0
+ 527.920396727 1705.00342151 527.920396727 1705.00342151 545.564126336 1676.01729429 c 0
+ 553.667102023 1662.70526281 553.667102023 1662.70526281 555.615786741 1658.80789337 c 0
+ 556.9883423 1656.06278225 556.9883423 1656.06278225 558.118524875 1653.46941152 c 0
+ 559.248707449 1650.87604078 559.248707449 1650.87604078 559.967222509 1649.02866899 c 0
+ 560.685737568 1647.18129719 560.685737568 1647.18129719 562.420306544 1642.60392319 c 0
+ 564.154875519 1638.02654919 564.154875519 1638.02654919 565.603655969 1634.30111375 c 2
+ 953.444670969 613.719473764 l 2
+ 968 577.573202114 968 577.573202114 968 555 c 0
+ 968 532.426797886 968 532.426797886 953.433067855 496.251711406 c 2
EndSplineSet
EndChar
EndChars