prefer explicit \<Zproject> (with its own Unicode codepoint);
authorwenzelm
Thu, 18 Mar 2021 12:41:17 +0100
changeset 73447 2200a19cac72
parent 73446 d1c4c2395650
child 73448 76a061b67993
prefer explicit \<Zproject> (with its own Unicode codepoint);
etc/symbols
lib/texinputs/isabellesym.sty
--- 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
--- 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}}}}