# HG changeset patch
# User wenzelm
# Date 1616067677 -3600
# Node ID 2200a19cac7214b3d75f43b17793cbd5dfa22cfc
# Parent  d1c4c23956502d55b7e0445abb8c981aa6da64ba
prefer explicit \<Zproject> (with its own Unicode codepoint);

diff -r d1c4c2395650 -r 2200a19cac72 etc/symbols
--- a/etc/symbols	Wed Mar 17 22:24:57 2021 +0100
+++ b/etc/symbols	Thu Mar 18 12:41:17 2021 +0100
@@ -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
+\<Zproject>             code: 0x002A21  group: Z_Notation  group: operator
 \<Ztypecolon>           code: 0x002982  group: Z_Notation  group: relation
 \<Zhide>                code: 0x0029F9  group: Z_Notation  group: operator
 \<Zcat>                 code: 0x002040  group: Z_Notation  group: operator
diff -r d1c4c2395650 -r 2200a19cac72 lib/texinputs/isabellesym.sty
--- a/lib/texinputs/isabellesym.sty	Wed Mar 17 22:24:57 2021 +0100
+++ b/lib/texinputs/isabellesym.sty	Thu Mar 18 12:41:17 2021 +0100
@@ -397,6 +397,7 @@
 \newcommand{\isasymZrres}{\isamath{\rhd}}  %requires amssymb
 \newcommand{\isasymZnrres}{\isaZhbar{\isamath{\rhd}}}  %requires amssymb
 \newcommand{\isasymZspot}{\isamath{\bullet}}
+\newcommand{\isasymZproject}{\isamath{\upharpoonright}}  %requires amssymb
 \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}}}}