support symbol \<Parallel>, based on \bigparallel from stdmaryd (stmary10.pfb: move y=1100, scale 222%, embolden by 40 units, adjust spacing);

--- a/Admin/components/components.sha1	Mon Oct 04 13:32:34 2021 +0200
+++ b/Admin/components/components.sha1	Mon Oct 04 13:39:38 2021 +0200
@@ -124,6 +124,7 @@
 b166b4bd583b6442a5d75eab06f7adbb66919d6d  isabelle_fonts-20210319.tar.gz
 9467ad54a9ac10a6e7e8db5458d8d2a5516eba96  isabelle_fonts-20210321.tar.gz
 1f7a0b9829ecac6552b21e995ad0f0ac168634f3  isabelle_fonts-20210322.tar.gz
+667000ce6dd6ea3c2d11601a41c206060468807d  isabelle_fonts-20211004.tar.gz
 916adccd2f40c55116b68b92ce1eccb24d4dd9a2  isabelle_setup-20210630.tar.gz
 c611e363287fcc9bdd93c33bef85fa4e66cd3f37  isabelle_setup-20210701.tar.gz
 a0e7527448ef0f7ce164a38a50dc26e98de3cad6  isabelle_setup-20210709.tar.gz

--- a/Admin/components/main	Mon Oct 04 13:32:34 2021 +0200
+++ b/Admin/components/main	Mon Oct 04 13:39:38 2021 +0200
@@ -7,7 +7,7 @@
 e-2.6
 flatlaf-1.6
 idea-icons-20210508
-isabelle_fonts-20210322
+isabelle_fonts-20211004
 isabelle_setup-20210922
 jdk-17+35
 jedit-20210802

--- a/Admin/isabelle_fonts/IsabelleSymbols.sfd	Mon Oct 04 13:32:34 2021 +0200
+++ b/Admin/isabelle_fonts/IsabelleSymbols.sfd	Mon Oct 04 13:39:38 2021 +0200
@@ -20,7 +20,7 @@
 OS2_WeightWidthSlopeOnly: 0
 OS2_UseTypoMetrics: 1
 CreationTime: 1050361371
-ModificationTime: 1616429436
+ModificationTime: 1633346733
 PfmFamily: 17
 TTFWeight: 400
 TTFWidth: 5
@@ -2242,11 +2242,11 @@
 DisplaySize: -96
 AntiAlias: 1
 FitToEm: 1
-WinInfo: 10980 12 6
+WinInfo: 8196 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 1462
+BeginChars: 1114189 1463
 
 StartChar: u10000
 Encoding: 65536 65536 0
@@ -63624,5 +63624,44 @@
  1271 1288 1271 1288 1271 1280 c 0,0,1
 EndSplineSet
 EndChar
+
+StartChar: uni2016
+Encoding: 8214 8214 1462
+Width: 1408
+VWidth: 3930
+Flags: W
+VStem: 324.48 188.739<-502.563 1702.56> 912.78 188.739<-500.697 1716.06>
+LayerCount: 2
+Fore
+SplineSet
+324.48046875 1636.74023438 m 2,0,1
+ 324.48046875 1676.40625 324.48046875 1676.40625 352.905273438 1703.41015625 c 0,2,3
+ 380.89453125 1730 380.89453125 1730 419.959960938 1730 c 0,4,5
+ 438.3125 1730 438.3125 1730 454.934570312 1722.7734375 c 128,-1,6
+ 471.557617188 1715.546875 471.557617188 1715.546875 485.162109375 1701.94238281 c 128,-1,7
+ 498.767578125 1688.3359375 498.767578125 1688.3359375 505.994140625 1671.71582031 c 128,-1,8
+ 513.219726562 1655.09667969 513.219726562 1655.09667969 513.219726562 1636.74023438 c 2,9,-1
+ 513.219726562 -436.740234375 l 2,10,11
+ 513.219726562 -473.883789062 513.219726562 -473.883789062 485.162109375 -501.94140625 c 128,-1,12
+ 457.104492188 -530 457.104492188 -530 419.959960938 -530 c 0,13,14
+ 380.89453125 -530 380.89453125 -530 352.904296875 -503.41015625 c 0,15,16
+ 324.48046875 -476.40625 324.48046875 -476.40625 324.48046875 -436.740234375 c 2,17,-1
+ 324.48046875 1636.74023438 l 2,0,1
+1101.51953125 -436.740234375 m 2,18,19
+ 1101.51953125 -473.584960938 1101.51953125 -473.584960938 1074.9296875 -501.57421875 c 0,20,21
+ 1047.92578125 -530 1047.92578125 -530 1008.25976562 -530 c 0,22,23
+ 969.194335938 -530 969.194335938 -530 941.206054688 -503.41015625 c 0,24,25
+ 912.780273438 -476.40625 912.780273438 -476.40625 912.780273438 -436.740234375 c 2,26,-1
+ 912.780273438 1636.74023438 l 2,27,28
+ 912.780273438 1656.08203125 912.780273438 1656.08203125 920.038085938 1673.13964844 c 128,-1,29
+ 927.295898438 1690.19628906 927.295898438 1690.19628906 941.205078125 1703.41015625 c 0,30,31
+ 969.194335938 1730 969.194335938 1730 1008.25976562 1730 c 0,32,33
+ 1027.6015625 1730 1027.6015625 1730 1044.65917969 1722.7421875 c 128,-1,34
+ 1061.71582031 1715.484375 1061.71582031 1715.484375 1074.9296875 1701.57421875 c 0,35,36
+ 1087.87402344 1687.94921875 1087.87402344 1687.94921875 1094.69628906 1671.43066406 c 128,-1,37
+ 1101.51953125 1654.91113281 1101.51953125 1654.91113281 1101.51953125 1636.74023438 c 2,38,-1
+ 1101.51953125 -436.740234375 l 2,18,19
+EndSplineSet
+EndChar
 EndChars
 EndSplineFont

--- a/Admin/isabelle_fonts/IsabelleSymbolsBold.sfd	Mon Oct 04 13:32:34 2021 +0200
+++ b/Admin/isabelle_fonts/IsabelleSymbolsBold.sfd	Mon Oct 04 13:39:38 2021 +0200
@@ -21,7 +21,7 @@
 OS2_WeightWidthSlopeOnly: 0
 OS2_UseTypoMetrics: 1
 CreationTime: 1050374980
-ModificationTime: 1616429477
+ModificationTime: 1633346753
 PfmFamily: 17
 TTFWeight: 700
 TTFWidth: 5
@@ -1679,10 +1679,10 @@
 DisplaySize: -96
 AntiAlias: 1
 FitToEm: 1
-WinInfo: 10978 11 8
+WinInfo: 8195 11 8
 BeginPrivate: 0
 EndPrivate
-BeginChars: 1114115 1450
+BeginChars: 1114115 1451
 
 StartChar: .notdef
 Encoding: 1114112 -1 0
@@ -71737,5 +71737,63 @@
  1131.20656165 1403 1131.20656165 1403 1167.81653987 1380.08960467 c 1,0,1
 EndSplineSet
 EndChar
+
+StartChar: uni2016
+Encoding: 8214 8214 1450
+Width: 1408
+VWidth: 3930
+Flags: W
+LayerCount: 2
+Fore
+SplineSet
+273.48046875 1636.74023438 m 2
+ 274.305963608 1698.42980182 274.305963608 1698.42980182 317.779016975 1740.38509515 c 0
+ 331.5651659 1753.48196068 331.5651659 1753.48196068 348.024849563 1762.58337143 c 0
+ 364.484533226 1771.68478217 364.484533226 1771.68478217 382.684388387 1776.34239109 c 0
+ 400.884243548 1781 400.884243548 1781 419.959960938 1781 c 0
+ 434.214451746 1781 434.214451746 1781 448.226135404 1778.10483503 c 0
+ 462.237819061 1775.20967007 462.237819061 1775.20967007 475.267592525 1769.544884 c 0
+ 500.772123393 1758.45726043 500.772123393 1758.45726043 521.225849377 1738.00353445 c 0
+ 527.877534153 1731.35137223 527.877534153 1731.35137223 533.617741307 1724.04056682 c 0
+ 539.357948462 1716.7297614 539.357948462 1716.7297614 544.207481245 1708.65391055 c 0
+ 549.057014029 1700.5780597 549.057014029 1700.5780597 552.764844573 1692.05055051 c 0
+ 564.219726562 1665.70385748 564.219726562 1665.70385748 564.219726562 1636.74023438 c 2
+ 564.219726562 -436.740234375 l 2
+ 564.219726562 -495.008680733 564.219726562 -495.008680733 521.225182787 -538.003224508 c 0
+ 507.658300589 -551.57057891 507.658300589 -551.57057891 491.595678193 -561.145395835 c 0
+ 475.533055797 -570.720212761 475.533055797 -570.720212761 457.267144636 -575.860106381 c 0
+ 439.001233476 -581 439.001233476 -581 419.959960938 -581 c 0
+ 391.253451691 -581 391.253451691 -581 364.896337999 -570.553783949 c 0
+ 338.539224308 -560.107567898 338.539224308 -560.107567898 317.777206298 -540.384302725 c 0
+ 296.387100388 -520.062746736 296.387100388 -520.062746736 284.933784569 -493.217738834 c 0
+ 273.48046875 -466.372730933 273.48046875 -466.372730933 273.48046875 -436.740234375 c 2
+ 273.48046875 1636.74023438 l 2
+1152.51953125 -436.740234375 m 2
+ 1151.74952957 -494.144209416 1151.74952957 -494.144209416 1111.90503919 -536.700040691 c 0
+ 1091.58360184 -558.091491525 1091.58360184 -558.091491525 1064.73824301 -569.545745762 c 0
+ 1037.89288418 -581 1037.89288418 -581 1008.25976562 -581 c 0
+ 979.553949558 -581 979.553949558 -581 953.196369328 -570.553430392 c 0
+ 926.838789099 -560.106860784 926.838789099 -560.106860784 906.080232746 -540.385507945 c 0
+ 861.780273438 -498.301459752 861.780273438 -498.301459752 861.780273438 -436.740234375 c 2
+ 861.780273438 1636.74023438 l 2
+ 861.780273438 1651.32239562 861.780273438 1651.32239562 864.624564811 1665.58641717 c 0
+ 867.468856184 1679.85043872 867.468856184 1679.85043872 873.10986998 1693.10818737 c 0
+ 878.772167602 1706.41519628 878.772167602 1706.41519628 887.133373164 1718.37257459 c 0
+ 895.494578727 1730.3299529 895.494578727 1730.3299529 906.078821663 1740.38509515 c 0
+ 948.831274571 1781 948.831274571 1781 1008.25976562 1781 c 0
+ 1038.00042276 1781 1038.00042276 1781 1064.62771862 1769.67040346 c 0
+ 1073.50484059 1765.89307777 1073.50484059 1765.89307777 1081.84644385 1760.86774412 c 0
+ 1090.18804712 1755.84241046 1090.18804712 1755.84241046 1097.70707391 1749.78666415 c 0
+ 1105.2261007 1743.73091784 1105.2261007 1743.73091784 1111.90386462 1736.70127707 c 0
+ 1116.65951952 1731.69555114 1116.65951952 1731.69555114 1120.93180299 1726.3118946 c 0
+ 1125.20408645 1720.92823807 1125.20408645 1720.92823807 1128.97353615 1715.18962916 c 0
+ 1132.74298584 1709.45102026 1132.74298584 1709.45102026 1135.97975475 1703.34407818 c 0
+ 1139.21652366 1697.2371361 1139.21652366 1697.2371361 1141.83366456 1690.90032844 c 0
+ 1145.36294721 1682.35569623 1145.36294721 1682.35569623 1147.74798058 1673.36655214 c 0
+ 1150.13301394 1664.37740804 1150.13301394 1664.37740804 1151.3262726 1655.19274645 c 0
+ 1152.51953125 1646.00808487 1152.51953125 1646.00808487 1152.51953125 1636.74023438 c 2
+ 1152.51953125 -436.740234375 l 2
+EndSplineSet
+EndChar
 EndChars
 EndSplineFont

--- a/NEWS	Mon Oct 04 13:32:34 2021 +0200
+++ b/NEWS	Mon Oct 04 13:39:38 2021 +0200
@@ -59,8 +59,8 @@
 
 *** Document preparation ***
 
-* More predefined symbols: \<interleave> \<sslash> (package "stmaryrd"), \<checkmark> \<crossmark> (LaTeX package
-"pifont").
+* More predefined symbols: \<Parallel> \<interleave> \<sslash> (package "stmaryrd"), \<checkmark> \<crossmark> (LaTeX
+package "pifont").
 
 * High-quality blackboard-bold symbols from font "txmia" (LaTeX package
 "pxfonts"): \<bbbA>\<bool>\<complex>\<bbbD>\<bbbE>\<bbbF>\<bbbG>\<bbbH>\<bbbI>\<bbbJ>\<bbbK>\<bbbL>\<bbbM>\<nat>\<bbbO>\<bbbP>\<rat>\<real>\<bbbS>\<bbbT>\<bbbU>\<bbbV>\<bbbW>\<bbbX>\<bbbY>\<int>.

--- a/etc/symbols	Mon Oct 04 13:32:34 2021 +0200
+++ b/etc/symbols	Mon Oct 04 13:39:38 2021 +0200
@@ -301,6 +301,7 @@
 \<preceq>               code: 0x00227c  group: relation
 \<succeq>               code: 0x00227d  group: relation
 \<parallel>             code: 0x002225  group: relation  abbrev: ||
+\<Parallel>             code: 0x002016  group: relation  abbrev: ||
 \<interleave>           code: 0x002af4  group: relation  abbrev: ||
 \<sslash>               code: 0x002afd  group: relation  abbrev: ||
 \<bar>                  code: 0x0000a6  group: punctuation  abbrev: ||

--- a/lib/texinputs/isabellesym.sty	Mon Oct 04 13:32:34 2021 +0200
+++ b/lib/texinputs/isabellesym.sty	Mon Oct 04 13:39:38 2021 +0200
@@ -303,6 +303,7 @@
 \newcommand{\isasympreceq}{\isamath{\preceq}}
 \newcommand{\isasymsucceq}{\isamath{\succeq}}
 \newcommand{\isasymparallel}{\isamath{\parallel}}
+\newcommand{\isasymParallel}{\isamath{\bigparallel}}  %requires stmaryrd
 \newcommand{\isasyminterleace}{\isamath{\interleave}}  %requires stmaryrd
 \newcommand{\isasymsslash}{\isamath{\sslash}}  %requires stmaryrd
 \newcommand{\isasymbar}{\isamath{\mid}}

--- a/src/Doc/Isar_Ref/document/root.tex	Mon Oct 04 13:32:34 2021 +0200
+++ b/src/Doc/Isar_Ref/document/root.tex	Mon Oct 04 13:39:38 2021 +0200
@@ -7,7 +7,7 @@
 \usepackage{eurosym}
 \usepackage{pifont}
 \usepackage[english]{babel}
-\usepackage[only,bigsqcap,fatsemi,interleave,sslash]{stmaryrd}
+\usepackage[only,bigsqcap,fatsemi,bigparallel,interleave,sslash]{stmaryrd}
 \usepackage{graphicx}
 \let\intorig=\int  %iman.sty redefines \int
 \usepackage{iman,extra,isar,proof}

--- a/src/Pure/Admin/build_fonts.scala	Mon Oct 04 13:32:34 2021 +0200
+++ b/src/Pure/Admin/build_fonts.scala	Mon Oct 04 13:39:38 2021 +0200
@@ -57,6 +57,7 @@
         0x2013,  // dash
         0x2014,  // dash
         0x2015,  // dash
+        0x2016,  // big parallel
         0x2020,  // dagger
         0x2021,  // double dagger
         0x2022,  // bullet

--- a/src/Pure/Tools/mkroot.scala	Mon Oct 04 13:32:34 2021 +0200
+++ b/src/Pure/Tools/mkroot.scala	Mon Oct 04 13:39:38 2021 +0200
@@ -85,8 +85,8 @@
 %\""" + """usepackage{eurosym}
   %for \<euro>
 
-%\""" + """usepackage[only,bigsqcap,fatsemi,interleave,sslash]{stmaryrd}
-  %for \<Sqinter>, \<Zsemi>
+%\""" + """usepackage[only,bigsqcap,fatsemi,interleave,sslash,bigparallel]{stmaryrd}
+  %for \<Sqinter>, \<Zsemi>, \<Parallel>
 
 %\""" + """usepackage{eufrak}
   %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)