# HG changeset patch
# User wenzelm
# Date 1616153755 -3600
# Node ID a9e0fae0107dcb15d88dc09435026dd07b9d70bf
# Parent  519ce76a602fd7a72bebc41fbce555c7b7fea780
more Z_Notation symbols, as proposed by Simon Foster;
some LaTeX-art based on tex.stackexchange "How do you make a square element symbol (\in)";

diff -r 519ce76a602f -r a9e0fae0107d etc/symbols
--- a/etc/symbols	Thu Mar 18 21:49:19 2021 +0100
+++ b/etc/symbols	Fri Mar 19 12:35:55 2021 +0100
@@ -201,18 +201,18 @@
 \<Down>                 code: 0x0021d3  group: arrow
 \<updown>               code: 0x002195  group: arrow
 \<Updown>               code: 0x0021d5  group: arrow
-\<langle>               code: 0x0027e8  group: punctuation  abbrev: <<
-\<rangle>               code: 0x0027e9  group: punctuation  abbrev: >>
-\<llangle>              code: 0x0027ea  group: punctuation  abbrev: <<
-\<rrangle>              code: 0x0027eb  group: punctuation  abbrev: >>
+\<langle>               code: 0x0027e8  group: punctuation  group: Z_Notation  abbrev: <<
+\<rangle>               code: 0x0027e9  group: punctuation  group: Z_Notation  abbrev: >>
+\<llangle>              code: 0x0027ea  group: punctuation  group: Z_Notation  abbrev: <<
+\<rrangle>              code: 0x0027eb  group: punctuation  group: Z_Notation  abbrev: >>
 \<lceil>                code: 0x002308  group: punctuation  abbrev: [.
 \<rceil>                code: 0x002309  group: punctuation  abbrev: .]
 \<lfloor>               code: 0x00230a  group: punctuation  abbrev: [.
 \<rfloor>               code: 0x00230b  group: punctuation  abbrev: .]
-\<lparr>                code: 0x002987  group: punctuation  abbrev: (|
-\<rparr>                code: 0x002988  group: punctuation  abbrev: |)
-\<lbrakk>               code: 0x0027e6  group: punctuation  abbrev: [|
-\<rbrakk>               code: 0x0027e7  group: punctuation  abbrev: |]
+\<lparr>                code: 0x002987  group: punctuation  group: Z_Notation  abbrev: (|
+\<rparr>                code: 0x002988  group: punctuation  group: Z_Notation  abbrev: |)
+\<lbrakk>               code: 0x0027e6  group: punctuation  group: Z_Notation  abbrev: [|
+\<rbrakk>               code: 0x0027e7  group: punctuation  group: Z_Notation  abbrev: |]
 \<lbrace>               code: 0x002983  group: punctuation  abbrev: {|
 \<rbrace>               code: 0x002984  group: punctuation  abbrev: |}
 \<lblot>                code: 0x002989  group: punctuation  group: Z_Notation  abbrev: <<
@@ -267,7 +267,7 @@
 \<Sqinter>              code: 0x002a05  group: operator  abbrev: INF
 \<setminus>             code: 0x002216  group: operator
 \<propto>               code: 0x00221d  group: operator
-\<uplus>                code: 0x00228e  group: operator
+\<uplus>                code: 0x00228e  group: operator  group: Z_Notation
 \<Uplus>                code: 0x002a04  group: operator
 \<noteq>                code: 0x002260  group: relation  abbrev: ~=
 \<sim>                  code: 0x00223c  group: relation
@@ -332,7 +332,7 @@
 \<partial>              code: 0x002202
 \<flat>                 code: 0x00266d
 \<natural>              code: 0x00266e
-\<sharp>                code: 0x00266f
+\<sharp>                code: 0x00266f  group: Z_Notation
 \<angle>                code: 0x002220
 \<copyright>            code: 0x0000a9
 \<registered>           code: 0x0000ae
@@ -385,6 +385,7 @@
 \<Ztypecolon>           code: 0x002982  group: Z_Notation  group: relation
 \<Zhide>                code: 0x0029F9  group: Z_Notation  group: operator
 \<Zcat>                 code: 0x002040  group: Z_Notation  group: operator
+\<Zinbag>               code: 0x0022FF  group: Z_Notation  group: relation
 \<hole>                 code: 0x002311
 \<newline>              code: 0x0023ce
 \<comment>              code: 0x002015  group: document  argument: space_cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
diff -r 519ce76a602f -r a9e0fae0107d lib/texinputs/isabellesym.sty
--- a/lib/texinputs/isabellesym.sty	Thu Mar 18 21:49:19 2021 +0100
+++ b/lib/texinputs/isabellesym.sty	Fri Mar 19 12:35:55 2021 +0100
@@ -395,6 +395,7 @@
 \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}}}}
+\newcommand{\isasymZinbag}{\isatext{\ooalign{\isamath{\sqsubset\mkern-1mu}\cr\isamath{-\mkern-1mu}\cr}}}
 
 \newcommand{\isasymhole}{\isatext{\normalfont\rmfamily\wasylozenge}}  %requires wasysym
 \newcommand{\isasymnewline}{\isatext{\fbox{$\hookleftarrow$}}}