
diff -r 0c666a0c57d7 -r aef235b965bb thys2/Journal/isabellesym.sty
--- a/thys2/Journal/isabellesym.sty	Fri Jan 07 22:25:26 2022 +0000
+++ b/thys2/Journal/isabellesym.sty	Fri Jan 07 22:28:23 2022 +0000
@@ -150,12 +150,32 @@
 \newcommand{\isasymPhi}{\isamath{\Phi}}
 \newcommand{\isasymPsi}{\isamath{\Psi}}
 \newcommand{\isasymOmega}{\isamath{\Omega}}
-\newcommand{\isasymbool}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{B}}}
-\newcommand{\isasymcomplex}{\isamath{\mathrm{C}\mkern-15mu{\phantom{\mathrm{t}}\vrule}\mkern9mu}}
-\newcommand{\isasymnat}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{N}}}
-\newcommand{\isasymrat}{\isamath{\mathrm{Q}\mkern-16mu{\phantom{\mathrm{t}}\vrule}\mkern10mu}}
-\newcommand{\isasymreal}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{R}}}
-\newcommand{\isasymint}{\isamath{\mathsf{Z}\mkern-7.5mu\mathsf{Z}}}
+\newcommand{\isasymbbbA}{\isamath{\bbbA}}  %requires font txmia from txfonts
+\newcommand{\isasymbool}{\isamath{\bbbB}}  %requires font txmia from txfonts
+\newcommand{\isasymcomplex}{\isamath{\bbbC}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbD}{\isamath{\bbbD}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbE}{\isamath{\bbbE}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbF}{\isamath{\bbbF}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbG}{\isamath{\bbbG}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbH}{\isamath{\bbbH}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbI}{\isamath{\bbbI}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbJ}{\isamath{\bbbJ}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbK}{\isamath{\bbbK}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbL}{\isamath{\bbbL}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbM}{\isamath{\bbbM}}  %requires font txmia from txfonts
+\newcommand{\isasymnat}{\isamath{\bbbN}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbO}{\isamath{\bbbO}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbP}{\isamath{\bbbP}}  %requires font txmia from txfonts
+\newcommand{\isasymrat}{\isamath{\bbbQ}}  %requires font txmia from txfonts
+\newcommand{\isasymreal}{\isamath{\bbbR}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbS}{\isamath{\bbbS}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbT}{\isamath{\bbbT}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbU}{\isamath{\bbbU}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbV}{\isamath{\bbbV}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbW}{\isamath{\bbbW}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbX}{\isamath{\bbbX}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbY}{\isamath{\bbbY}}  %requires font txmia from txfonts
+\newcommand{\isasymint}{\isamath{\bbbZ}}  %requires font txmia from txfonts
 \newcommand{\isasymleftarrow}{\isamath{\leftarrow}}
 \newcommand{\isasymrightarrow}{\isamath{\rightarrow}}
 \newcommand{\isasymlongleftarrow}{\isamath{\longleftarrow}}
@@ -206,14 +226,16 @@
 \newcommand{\isasymrceil}{\isamath{\rceil}}
 \newcommand{\isasymlfloor}{\isamath{\lfloor}}
 \newcommand{\isasymrfloor}{\isamath{\rfloor}}
-\newcommand{\isasymlparr}{\isamath{\mathopen{(\mkern-3mu\mid}}}
-\newcommand{\isasymrparr}{\isamath{\mathclose{\mid\mkern-3mu)}}}
+\newcommand{\isasymlparr}{\isamath{\mathopen{(\mkern-3.3mu\mid}}}
+\newcommand{\isasymrparr}{\isamath{\mathclose{\mid\mkern-3.3mu)}}}
 \newcommand{\isasymlbrakk}{\isamath{\mathopen{\lbrack\mkern-3mu\lbrack}}}
 \newcommand{\isasymrbrakk}{\isamath{\mathclose{\rbrack\mkern-3mu\rbrack}}}
-\newcommand{\isasymlbrace}{\isamath{\mathopen{\lbrace\mkern-4.5mu\mid}}}
-\newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.5mu\rbrace}}}
-\newcommand{\isasymguillemotleft}{\isatext{\flqq}}  %requires babel
-\newcommand{\isasymguillemotright}{\isatext{\frqq}}  %requires babel
+\newcommand{\isasymlbrace}{\isamath{\mathopen{\lbrace\mkern-4.3mu\mid}}}
+\newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.3mu\rbrace}}}
+\newcommand{\isasymlblot}{\isamath{{\langle}\mkern -3.5mu{|}}}
+\newcommand{\isasymrblot}{\isamath{{|}\mkern -3.5mu{\rangle}}}
+\newcommand{\isasymguillemotleft}{\isatext{\guillemotleft}}
+\newcommand{\isasymguillemotright}{\isatext{\guillemotright}}
 \newcommand{\isasymbottom}{\isamath{\bot}}
 \newcommand{\isasymtop}{\isamath{\top}}
 \newcommand{\isasymand}{\isamath{\wedge}}
@@ -281,6 +303,9 @@
 \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}}
 \newcommand{\isasymbbar}{\isamath{[\mskip-1.5mu]}}
 \newcommand{\isasymplusminus}{\isamath{\pm}}
@@ -364,14 +389,44 @@
 \newcommand{\isasymsome}{\isamath{\epsilon\,}}
 \newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}}
 \newcommand{\isasymthen}{\isamath{\mathbin{>\!\!\!>}}}
-\newcommand{\isasymopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}
-\newcommand{\isasymclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}
+
+%Z notation
+\newcommand{\isaZhbar}[1]{\rlap{\raise.0001ex\hbox{\isamath{-}}}#1}
+\newcommand{\isaZpvbar}[1]{\ooalign{\hfil\isamath{\mapstochar\mkern 5mu}\hfil\cr#1}}
+\newcommand{\isaZfvbar}[1]{\ooalign{\hfil\isamath{\mapstochar\mkern 3mu\mapstochar\mkern 5mu}\hfil\cr#1}}
+\newcommand{\isaZdarrow}[3]{\ooalign{\isamath{#1}\hfil\cr\isamath{\mkern#3mu\isamath{#2}}}}
+\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
+\newcommand{\isasymZsurj}{\isaZdarrow{\rightarrow}{\rightarrow}{4}}  %requires amssymb
+\newcommand{\isasymZpsurj}{\isaZpvbar{\isasymZsurj}}  %requires amssymb
+\newcommand{\isasymZbij}{\isaZdarrow{\rightarrowtail}{\rightarrow}{5}}  %requires amssymb
+\newcommand{\isasymZpfun}{\isaZpvbar{\isamath{\rightarrow}}}
+\newcommand{\isasymZffun}{\isaZfvbar{\isamath{\rightarrow}}}
+\newcommand{\isasymZdres}{\isamath{\lhd}}  %requires amssymb
+\newcommand{\isasymZndres}{\isaZhbar{\isamath{\lhd}}}  %requires amssymb
+\newcommand{\isasymZrres}{\isamath{\rhd}}  %requires amssymb
+\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}}}}
+\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$}}}
 \newcommand{\isasymcomment}{\isatext{\isastylecmt---}}
 \newcommand{\isasymproof}{\isamath{\,\langle\mathit{proof}\rangle}}
-
+\newcommand{\isasymopen}{\isatext{\guilsinglleft}}
+\newcommand{\isasymclose}{\isatext{\guilsinglright}}
+\newcommand{\isasymcheckmark}{\isatext{\ding{51}}}  %requires pifont
+\newcommand{\isasymcrossmark}{\isatext{\ding{55}}}  %requires pifont
 \newcommand{\isactrlmarker}{\isatext{\ding{48}}}  %requires pifont
+\newcommand{\isactrltry}{\isakeywordcontrol{try}}
+\newcommand{\isactrlcan}{\isakeywordcontrol{can}}
 \newcommand{\isactrlassert}{\isakeywordcontrol{assert}}
 \newcommand{\isactrlcancel}{\isakeywordcontrol{cancel}}
 \newcommand{\isactrlbinding}{\isakeywordcontrol{binding}}
@@ -389,9 +444,12 @@
 \newcommand{\isactrldir}{\isakeywordcontrol{dir}}
 \newcommand{\isactrlfile}{\isakeywordcontrol{file}}
 \newcommand{\isactrlhere}{\isakeywordcontrol{here}}
+\newcommand{\isactrlinstantiate}{\isakeywordcontrol{instantiate}}
 \newcommand{\isactrlkeyword}{\isakeywordcontrol{keyword}}
 \newcommand{\isactrllatex}{\isakeywordcontrol{latex}}
 \newcommand{\isactrllocale}{\isakeywordcontrol{locale}}
+\newcommand{\isactrlmakeUNDERSCOREjudgment}{\isakeywordcontrol{make{\isacharunderscore}judgment}}
+\newcommand{\isactrldestUNDERSCOREjudgment}{\isakeywordcontrol{dest{\isacharunderscore}judgment}}
 \newcommand{\isactrlmakeUNDERSCOREstring}{\isakeywordcontrol{make{\isacharunderscore}string}}
 \newcommand{\isactrlmasterUNDERSCOREdir}{\isakeywordcontrol{master{\isacharunderscore}dir}}
 \newcommand{\isactrlmethod}{\isakeywordcontrol{method}}
@@ -420,8 +478,19 @@
 \newcommand{\isactrltypeUNDERSCOREname}{\isakeywordcontrol{type{\isacharunderscore}name}}
 \newcommand{\isactrltypeUNDERSCOREsyntax}{\isakeywordcontrol{type{\isacharunderscore}syntax}}
 \newcommand{\isactrlundefined}{\isakeywordcontrol{undefined}}
+\newcommand{\isactrltvar}{\isakeywordcontrol{tvar}}
+\newcommand{\isactrlvar}{\isakeywordcontrol{var}}
+\newcommand{\isactrlConst}{\isakeywordcontrol{Const}}
+\newcommand{\isactrlConstUNDERSCORE}{\isakeywordcontrol{Const{\isacharunderscore}}}
+\newcommand{\isactrlConstUNDERSCOREfn}{\isakeywordcontrol{Const{\isacharunderscore}fn}}
+\newcommand{\isactrlType}{\isakeywordcontrol{Type}}
+\newcommand{\isactrlTypeUNDERSCOREfn}{\isakeywordcontrol{Type{\isacharunderscore}fn}}
 
 \newcommand{\isactrlcode}{\isakeywordcontrol{code}}
 \newcommand{\isactrlcomputation}{\isakeywordcontrol{computation}}
 \newcommand{\isactrlcomputationUNDERSCOREconv}{\isakeywordcontrol{computation{\isacharunderscore}conv}}
 \newcommand{\isactrlcomputationUNDERSCOREcheck}{\isakeywordcontrol{computation{\isacharunderscore}check}}
+\newcommand{\isactrlifUNDERSCORElinux}{\isakeywordcontrol{if{\isacharunderscore}linux}}
+\newcommand{\isactrlifUNDERSCOREmacos}{\isakeywordcontrol{if{\isacharunderscore}macos}}
+\newcommand{\isactrlifUNDERSCOREwindows}{\isakeywordcontrol{if{\isacharunderscore}windows}}
+\newcommand{\isactrlifUNDERSCOREunix}{\isakeywordcontrol{if{\isacharunderscore}unix}}




