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