# HG changeset patch
# User wenzelm
# Date 1616157873 -3600
# Node ID 0cc9c2d439577b64ddaf620d91227950a8125c5c
# Parent  b134f9dbe4b78acade5db478824eb9ca721a08d0
clarified \<Zcomp> (small) vs. \<Zsemi> (big);

diff -r b134f9dbe4b7 -r 0cc9c2d43957 etc/symbols
--- a/etc/symbols	Fri Mar 19 13:22:12 2021 +0100
+++ b/etc/symbols	Fri Mar 19 13:44:33 2021 +0100
@@ -367,7 +367,7 @@
 \<bind>                 code: 0x00291c  group: operator  abbrev: >>=
 \<then>                 code: 0x002aa2  group: operator  group: Z_Notation  abbrev: >>
 \<some>                 code: 0x0003f5
-\<Zsemi>                code: 0x002A1F  group: Z_Notation  group: punctuation
+\<Zcomp>                code: 0x002A3E  group: Z_Notation  group: punctuation
 \<Zinj>                 code: 0x0021A3  group: Z_Notation  group: arrow  abbrev: .>
 \<Zpinj>                code: 0x002914  group: Z_Notation  group: arrow  abbrev: .>
 \<Zfinj>                code: 0x002915  group: Z_Notation  group: arrow  abbrev: .>
@@ -381,6 +381,7 @@
 \<Zrres>                code: 0x0025B7  group: Z_Notation  group: relation
 \<Znrres>               code: 0x002A65  group: Z_Notation  group: relation
 \<Zspot>                code: 0x002981  group: Z_Notation  group: punctuation
+\<Zsemi>                code: 0x002A1F  group: Z_Notation  group: punctuation
 \<Zproject>             code: 0x002A21  group: Z_Notation  group: operator
 \<Ztypecolon>           code: 0x002982  group: Z_Notation  group: relation
 \<Zhide>                code: 0x0029F9  group: Z_Notation  group: operator
diff -r b134f9dbe4b7 -r 0cc9c2d43957 lib/texinputs/isabellesym.sty
--- a/lib/texinputs/isabellesym.sty	Fri Mar 19 13:22:12 2021 +0100
+++ b/lib/texinputs/isabellesym.sty	Fri Mar 19 13:44:33 2021 +0100
@@ -377,7 +377,7 @@
 \newcommand{\isasymZarithmos}{\isamath{\mathbb A}}  %requires amssymb
 \newcommand{\isasymZuniv}{\isamath{\mathbb U}}  %requires amssymb
 \newcommand{\isasymZworld}{\isamath{\mathbb W}}  %requires amssymb
-\newcommand{\isasymZsemi}{\isamath{\fatsemi}}  %requires stmaryrd
+\newcommand{\isasymZcomp}{\isamath{\fatsemi}}  %requires stmaryrd
 \newcommand{\isasymZinj}{\isamath{\rightarrowtail}}  %requires amssymb
 \newcommand{\isasymZpinj}{\isaZpvbar{\isamath{\rightarrowtail}}}  %requires amssymb
 \newcommand{\isasymZfinj}{\isaZfvbar{\isasymZinj}}  %requires amssymb
@@ -392,6 +392,7 @@
 \newcommand{\isasymZnrres}{\isaZhbar{\isamath{\rhd}}}  %requires amssymb
 \newcommand{\isasymZspot}{\isamath{\bullet}}
 \newcommand{\isasymZproject}{\isamath{\upharpoonright}}  %requires amssymb
+\newcommand{\isasymZsemi}{\isatext{\raise 0.66ex\hbox{\oalign{\hfil\isamath{\scriptscriptstyle\mathrm{o}}\hfil\cr\hfil\isamath{\scriptscriptstyle\mathrm{9}}\hfil}}}}
 \newcommand{\isasymZtypecolon}{\isatext{\raise 0.6ex\hbox{\oalign{\hfil\isamath{\scriptscriptstyle\mathrm{o}}\hfil\cr\hfil\isamath{\scriptscriptstyle\mathrm{o}}\hfil}}}}
 \newcommand{\isasymZhide}{\isamath{\backslash}}
 \newcommand{\isasymZcat}{\isatext{\raise 0.8ex\hbox{\isamath{\mathchar\frown}}}}