# HG changeset patch
# User wenzelm
# Date 1616430282 -3600
# Node ID 090add96f5f90764fb13d534cc7213340ec233bd
# Parent  ee1c4962671cd236648a64eff7be90856b6531f7
more glyphs proposed by Simon Foster: 0x002713, 0x002717, 0x002af4, 0x002afb, 0x002afd;
corresponding symbols and latex macros;

diff -r ee1c4962671c -r 090add96f5f9 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Mon Mar 22 10:49:51 2021 +0000
+++ b/Admin/components/components.sha1	Mon Mar 22 17:24:42 2021 +0100
@@ -114,6 +114,7 @@
 3ff9195aab574fc75ca3b77af0adb33f9b6d7b74  isabelle_fonts-20210318.tar.gz
 b166b4bd583b6442a5d75eab06f7adbb66919d6d  isabelle_fonts-20210319.tar.gz
 9467ad54a9ac10a6e7e8db5458d8d2a5516eba96  isabelle_fonts-20210321.tar.gz
+1f7a0b9829ecac6552b21e995ad0f0ac168634f3  isabelle_fonts-20210322.tar.gz
 0b2206f914336dec4923dd0479d8cee4b904f544  jdk-11+28.tar.gz
 e12574d838ed55ef2845acf1152329572ab0cc56  jdk-11.0.10+9.tar.gz
 3e05213cad47dbef52804fe329395db9b4e57f39  jdk-11.0.2+9.tar.gz
diff -r ee1c4962671c -r 090add96f5f9 Admin/components/main
--- a/Admin/components/main	Mon Mar 22 10:49:51 2021 +0000
+++ b/Admin/components/main	Mon Mar 22 17:24:42 2021 +0100
@@ -5,7 +5,7 @@
 cvc4-1.8
 e-2.5-1
 flatlaf-1.0
-isabelle_fonts-20210321
+isabelle_fonts-20210322
 jdk-15.0.2+7
 jedit_build-20210201
 jfreechart-1.5.1
diff -r ee1c4962671c -r 090add96f5f9 Admin/isabelle_fonts/IsabelleSymbols.sfd
--- a/Admin/isabelle_fonts/IsabelleSymbols.sfd	Mon Mar 22 10:49:51 2021 +0000
+++ b/Admin/isabelle_fonts/IsabelleSymbols.sfd	Mon Mar 22 17:24:42 2021 +0100
@@ -20,7 +20,7 @@
 OS2_WeightWidthSlopeOnly: 0
 OS2_UseTypoMetrics: 1
 CreationTime: 1050361371
-ModificationTime: 1616358903
+ModificationTime: 1616429436
 PfmFamily: 17
 TTFWeight: 400
 TTFWidth: 5
@@ -2242,11 +2242,11 @@
 DisplaySize: -96
 AntiAlias: 1
 FitToEm: 1
-WinInfo: 120112 16 4
+WinInfo: 10980 12 6
 BeginPrivate: 0
 EndPrivate
 TeXData: 1 0 0 631296 315648 210432 572416 -1048576 210432 783286 444596 497025 792723 393216 433062 380633 303038 157286 324010 404750 52429 2506097 1059062 262144
-BeginChars: 1114189 1458
+BeginChars: 1114189 1462
 
 StartChar: u10000
 Encoding: 65536 65536 0
@@ -62450,31 +62450,32 @@
 StartChar: uni2AF4
 Encoding: 10996 10996 1438
 Width: 1422
-Flags: W
-LayerCount: 2
-Fore
-SplineSet
-1150 -205 m 2,0,1
- 1150 -242 1150 -242 1109 -242 c 256,2,3
- 1068 -242 1068 -242 1068 -205 c 2,4,-1
- 1068 1369 l 2,5,6
- 1068 1406 1068 1406 1109 1406 c 256,7,8
- 1150 1406 1150 1406 1150 1369 c 2,9,-1
- 1150 -205 l 2,0,1
-752 -205 m 2,10,11
- 752 -242 752 -242 711 -242 c 256,12,13
- 670 -242 670 -242 670 -205 c 2,14,-1
- 670 1369 l 2,15,16
- 670 1406 670 1406 711 1406 c 256,17,18
- 752 1406 752 1406 752 1369 c 2,19,-1
- 752 -205 l 2,10,11
-354 -205 m 2,20,21
- 354 -242 354 -242 313 -242 c 256,22,23
- 272 -242 272 -242 272 -205 c 2,24,-1
- 272 1369 l 2,25,26
- 272 1406 272 1406 313 1406 c 256,27,28
- 354 1406 354 1406 354 1369 c 2,29,-1
- 354 -205 l 2,20,21
+VWidth: 2121
+Flags: W
+LayerCount: 2
+Fore
+SplineSet
+1150 -454.349609375 m 2,0,1
+ 1150 -493.200195312 1150 -493.200195312 1109 -493.200195312 c 256,2,3
+ 1068 -493.200195312 1068 -493.200195312 1068 -454.349609375 c 2,4,-1
+ 1068 1618.34960938 l 2,5,6
+ 1068 1657.20019531 1068 1657.20019531 1109 1657.20019531 c 256,7,8
+ 1150 1657.20019531 1150 1657.20019531 1150 1618.34960938 c 2,9,-1
+ 1150 -454.349609375 l 2,0,1
+752 -454.349609375 m 2,10,11
+ 752 -493.200195312 752 -493.200195312 711 -493.200195312 c 256,12,13
+ 670 -493.200195312 670 -493.200195312 670 -454.349609375 c 2,14,-1
+ 670 1618.34960938 l 2,15,16
+ 670 1657.20019531 670 1657.20019531 711 1657.20019531 c 256,17,18
+ 752 1657.20019531 752 1657.20019531 752 1618.34960938 c 2,19,-1
+ 752 -454.349609375 l 2,10,11
+354 -454.349609375 m 2,20,21
+ 354 -493.200195312 354 -493.200195312 313 -493.200195312 c 256,22,23
+ 272 -493.200195312 272 -493.200195312 272 -454.349609375 c 2,24,-1
+ 272 1618.34960938 l 2,25,26
+ 272 1657.20019531 272 1657.20019531 313 1657.20019531 c 256,27,28
+ 354 1657.20019531 354 1657.20019531 354 1618.34960938 c 2,29,-1
+ 354 -454.349609375 l 2,20,21
 EndSplineSet
 EndChar
 
@@ -63470,5 +63471,158 @@
  916.490234375 850.780273438 l 1,44,-1
 EndSplineSet
 EndChar
+
+StartChar: uni2AFB
+Encoding: 11003 11003 1458
+Width: 1565
+Flags: W
+LayerCount: 2
+Fore
+SplineSet
+1517 1568 m 0,0,1
+ 1517 1559 1517 1559 1509 1532 c 2,2,-1
+ 933 -395 l 2,3,4
+ 919 -442 919 -442 890 -442 c 0,5,6
+ 848 -442 848 -442 848 -404 c 0,7,8
+ 848 -395 848 -395 856 -368 c 2,9,-1
+ 1432 1559 l 2,10,11
+ 1446 1606 1446 1606 1475 1606 c 0,12,13
+ 1517 1606 1517 1606 1517 1568 c 0,0,1
+1117 1568 m 0,14,15
+ 1117 1559 1117 1559 1109 1532 c 2,16,-1
+ 533 -395 l 2,17,18
+ 519 -442 519 -442 490 -442 c 0,19,20
+ 448 -442 448 -442 448 -404 c 0,21,22
+ 448 -395 448 -395 456 -368 c 2,23,-1
+ 1032 1559 l 2,24,25
+ 1046 1606 1046 1606 1075 1606 c 0,26,27
+ 1117 1606 1117 1606 1117 1568 c 0,14,15
+717 1568 m 0,28,29
+ 717 1559 717 1559 709 1532 c 2,30,-1
+ 133 -395 l 2,31,32
+ 119 -442 119 -442 90 -442 c 0,33,34
+ 48 -442 48 -442 48 -404 c 0,35,36
+ 48 -395 48 -395 56 -368 c 2,37,-1
+ 632 1559 l 2,38,39
+ 646 1606 646 1606 675 1606 c 0,40,41
+ 717 1606 717 1606 717 1568 c 0,28,29
+EndSplineSet
+EndChar
+
+StartChar: uni2AFD
+Encoding: 11005 11005 1459
+Width: 1150
+Flags: W
+LayerCount: 2
+Fore
+SplineSet
+1105 1568 m 0,0,1
+ 1105 1559 1105 1559 1097 1532 c 2,2,-1
+ 521 -395 l 2,3,4
+ 507 -442 507 -442 478 -442 c 0,5,6
+ 436 -442 436 -442 436 -404 c 0,7,8
+ 436 -395 436 -395 444 -368 c 2,9,-1
+ 1020 1559 l 2,10,11
+ 1034 1606 1034 1606 1063 1606 c 0,12,13
+ 1105 1606 1105 1606 1105 1568 c 0,0,1
+705 1568 m 0,14,15
+ 705 1559 705 1559 697 1532 c 2,16,-1
+ 121 -395 l 2,17,18
+ 107 -442 107 -442 78 -442 c 0,19,20
+ 36 -442 36 -442 36 -404 c 0,21,22
+ 36 -395 36 -395 44 -368 c 2,23,-1
+ 620 1559 l 2,24,25
+ 634 1606 634 1606 663 1606 c 0,26,27
+ 705 1606 705 1606 705 1568 c 0,14,15
+EndSplineSet
+EndChar
+
+StartChar: uni2713
+Encoding: 10003 10003 1460
+Width: 1607
+Flags: W
+LayerCount: 2
+Fore
+SplineSet
+1507 1411 m 1,0,-1
+ 1317 1186 l 1,1,-1
+ 891 623 l 1,2,-1
+ 596 166 l 1,3,-1
+ 524 43 l 2,4,5
+ 513 21 513 21 481 -14 c 1,6,7
+ 453 -27 453 -27 364 -27 c 0,8,9
+ 287 -27 287 -27 273 -19 c 0,10,11
+ 256 -10 256 -10 225 55 c 0,12,13
+ 100 314 100 314 100 457 c 0,14,15
+ 100 493 100 493 147 526 c 0,16,17
+ 241 592 241 592 305 592 c 0,18,19
+ 331 592 331 592 344 570 c 0,20,21
+ 353 547 353 547 362 524 c 2,22,-1
+ 403 428 l 2,23,24
+ 435 354 435 354 450 354 c 0,25,26
+ 461 354 461 354 503 416 c 2,27,-1
+ 977 1118 l 1,28,-1
+ 1142 1321 l 2,29,30
+ 1190 1380 1190 1380 1302 1415 c 0,31,32
+ 1398 1444 1398 1444 1493 1444 c 1,33,-1
+ 1507 1411 l 1,0,-1
+EndSplineSet
+EndChar
+
+StartChar: uni2717
+Encoding: 10007 10007 1461
+Width: 1371
+Flags: W
+LayerCount: 2
+Fore
+SplineSet
+1271 1280 m 0,0,1
+ 1271 1268 1271 1268 1249 1247 c 0,2,3
+ 1231 1230 1231 1230 1179 1163 c 2,4,-1
+ 866 754 l 1,5,-1
+ 929 627 l 1,6,-1
+ 1089 285 l 1,7,8
+ 1080 264 1080 264 1061 256 c 1,9,-1
+ 1061 240 l 2,10,11
+ 1060 239 1060 239 1037 225 c 0,12,13
+ 1020 214 1020 214 1020 207 c 0,14,15
+ 1020 198 1020 198 1030 178 c 1,16,17
+ 1027 160 1027 160 1004 143.5 c 128,-1,18
+ 981 127 981 127 962 127 c 0,19,20
+ 942 127 942 127 884 217 c 2,21,-1
+ 692 514 l 1,22,-1
+ 286 -115 l 1,23,24
+ 254 -139 254 -139 180 -139 c 0,25,26
+ 163 -139 163 -139 137 -98 c 0,27,28
+ 106 -49 106 -49 106 -35 c 0,29,30
+ 106 -23 106 -23 112 -2 c 0,31,32
+ 121 29 121 29 110.5 38.5 c 128,-1,33
+ 100 48 100 48 100 53 c 0,34,35
+ 100 70 100 70 149 154 c 2,36,-1
+ 198 238 l 2,37,38
+ 277 373 277 373 549 702 c 2,39,-1
+ 573 731 l 1,40,-1
+ 422 1149 l 2,41,42
+ 399 1213 399 1213 399 1219 c 0,43,44
+ 399 1228 399 1228 426 1262 c 1,45,-1
+ 440 1274 l 2,46,47
+ 447 1280 447 1280 454 1280 c 0,48,49
+ 465 1280 465 1280 487 1262 c 1,50,51
+ 499 1272 499 1272 520 1272 c 0,52,53
+ 526 1275 526 1275 538 1286 c 1,54,55
+ 548 1303 548 1303 561 1303 c 0,56,57
+ 580 1303 580 1303 598 1266 c 2,58,-1
+ 753 958 l 1,59,-1
+ 805 1022 l 1,60,-1
+ 905 1137 l 2,61,62
+ 1092 1352 1092 1352 1101 1352 c 0,63,64
+ 1126 1352 1126 1352 1173 1313 c 1,65,-1
+ 1196 1333 l 1,66,67
+ 1210 1354 1210 1354 1218 1354 c 0,68,69
+ 1223 1354 1223 1354 1230 1337 c 0,70,71
+ 1234 1328 1234 1328 1254 1306 c 0,72,73
+ 1271 1288 1271 1288 1271 1280 c 0,0,1
+EndSplineSet
+EndChar
 EndChars
 EndSplineFont
diff -r ee1c4962671c -r 090add96f5f9 Admin/isabelle_fonts/IsabelleSymbolsBold.sfd
--- 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
diff -r ee1c4962671c -r 090add96f5f9 Admin/isabelle_fonts/README
--- a/Admin/isabelle_fonts/README	Mon Mar 22 10:49:51 2021 +0000
+++ b/Admin/isabelle_fonts/README	Mon Mar 22 17:24:42 2021 +0100
@@ -20,7 +20,7 @@
 
 
     Makarius
-    21-Mar-2021
+    22-Mar-2021
 
 
 ----------------------------------------------------------------------------
diff -r ee1c4962671c -r 090add96f5f9 etc/symbols
--- a/etc/symbols	Mon Mar 22 10:49:51 2021 +0000
+++ b/etc/symbols	Mon Mar 22 17:24:42 2021 +0100
@@ -301,6 +301,8 @@
 \<preceq>               code: 0x00227c  group: relation
 \<succeq>               code: 0x00227d  group: relation
 \<parallel>             code: 0x002225  group: punctuation  abbrev: ||
+\<interleave>           code: 0x002af4  group: punctuation  abbrev: ||
+\<sslash>               code: 0x002afd  group: punctuation  abbrev: ||
 \<bar>                  code: 0x0000a6  group: punctuation  abbrev: ||
 \<bbar>                 code: 0x002aff  group: punctuation  abbrev: ||
 \<plusminus>            code: 0x0000b1  group: operator
@@ -409,6 +411,8 @@
 \<^cancel>              code: 0x002326  group: document  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
 \<^latex>                               group: document  argument: cartouche
 \<^marker>              code: 0x002710  group: document  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
+\<checkmark>            code: 0x002713
+\<crossmark>            code: 0x002717
 \<open>                 code: 0x002039  group: punctuation  font: Isabelle␣DejaVu␣Sans␣Mono  abbrev: <<
 \<close>                code: 0x00203a  group: punctuation  font: Isabelle␣DejaVu␣Sans␣Mono  abbrev: >>
 \<^here>                code: 0x002302  font: Isabelle␣DejaVu␣Sans␣Mono
diff -r ee1c4962671c -r 090add96f5f9 lib/texinputs/isabellesym.sty
--- a/lib/texinputs/isabellesym.sty	Mon Mar 22 10:49:51 2021 +0000
+++ b/lib/texinputs/isabellesym.sty	Mon Mar 22 17:24:42 2021 +0100
@@ -303,6 +303,8 @@
 \newcommand{\isasympreceq}{\isamath{\preceq}}
 \newcommand{\isasymsucceq}{\isamath{\succeq}}
 \newcommand{\isasymparallel}{\isamath{\parallel}}
+\newcommand{\isasyminterleace}{\isamath{\interleave}}  %requires stmaryrd
+\newcommand{\isasymsslash}{\isamath{\sslash}}  %requires stmaryrd
 \newcommand{\isasymbar}{\isamath{\mid}}
 \newcommand{\isasymbbar}{\isamath{[\mskip-1.5mu]}}
 \newcommand{\isasymplusminus}{\isamath{\pm}}
@@ -416,10 +418,11 @@
 \newcommand{\isasymhole}{\isatext{\normalfont\rmfamily\wasylozenge}}  %requires wasysym
 \newcommand{\isasymnewline}{\isatext{\fbox{$\hookleftarrow$}}}
 \newcommand{\isasymcomment}{\isatext{\isastylecmt---}}
+\newcommand{\isasymproof}{\isamath{\,\langle\mathit{proof}\rangle}}
 \newcommand{\isasymopen}{\isatext{\guilsinglleft}}
 \newcommand{\isasymclose}{\isatext{\guilsinglright}}
-\newcommand{\isasymproof}{\isamath{\,\langle\mathit{proof}\rangle}}
-
+\newcommand{\isasymcheckmark}{\isatext{\ding{51}}}  %requires pifont
+\newcommand{\isasymcrossmark}{\isatext{\ding{55}}}  %requires pifont
 \newcommand{\isactrlmarker}{\isatext{\ding{48}}}  %requires pifont
 \newcommand{\isactrlassert}{\isakeywordcontrol{assert}}
 \newcommand{\isactrlcancel}{\isakeywordcontrol{cancel}}
diff -r ee1c4962671c -r 090add96f5f9 src/Doc/Isar_Ref/document/root.tex
--- a/src/Doc/Isar_Ref/document/root.tex	Mon Mar 22 10:49:51 2021 +0000
+++ b/src/Doc/Isar_Ref/document/root.tex	Mon Mar 22 17:24:42 2021 +0100
@@ -7,7 +7,7 @@
 \usepackage{eurosym}
 \usepackage{pifont}
 \usepackage[english]{babel}
-\usepackage[only,bigsqcap,fatsemi]{stmaryrd}
+\usepackage[only,bigsqcap,fatsemi,interleave,sslash]{stmaryrd}
 \usepackage{graphicx}
 \let\intorig=\int  %iman.sty redefines \int
 \usepackage{iman,extra,isar,proof}
diff -r ee1c4962671c -r 090add96f5f9 src/Pure/Admin/build_fonts.scala
--- a/src/Pure/Admin/build_fonts.scala	Mon Mar 22 10:49:51 2021 +0000
+++ b/src/Pure/Admin/build_fonts.scala	Mon Mar 22 17:24:42 2021 +0100
@@ -90,6 +90,8 @@
         0x266d,  // musical flat
         0x266e,  // musical natural
         0x266f,  // musical sharp
+        0x2713,  // check mark
+        0x2717,  // ballot X
         0x2756,  // UNDEFINED
         0x2759,  // BOLD
         0x27a7,  // DESCR
diff -r ee1c4962671c -r 090add96f5f9 src/Pure/Tools/mkroot.scala
--- a/src/Pure/Tools/mkroot.scala	Mon Mar 22 10:49:51 2021 +0000
+++ b/src/Pure/Tools/mkroot.scala	Mon Mar 22 17:24:42 2021 +0100
@@ -85,7 +85,7 @@
 %\""" + """usepackage{eurosym}
   %for \<euro>
 
-%\""" + """usepackage[only,bigsqcap,fatsemi]{stmaryrd}
+%\""" + """usepackage[only,bigsqcap,fatsemi,interleave,sslash]{stmaryrd}
   %for \<Sqinter>, \<Zsemi>
 
 %\""" + """usepackage{eufrak}