--- 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}}