diff -r 0c666a0c57d7 -r aef235b965bb thys2/Journal/isabelle.sty
--- a/thys2/Journal/isabelle.sty	Fri Jan 07 22:25:26 2022 +0000
+++ b/thys2/Journal/isabelle.sty	Fri Jan 07 22:28:23 2022 +0000
@@ -39,6 +39,36 @@
 \DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}
 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
 
+%blackboard-bold (requires font txmia from pxfonts)
+\DeclareSymbolFont{bbbfont}{U}{txmia}{m}{it}
+\SetSymbolFont{bbbfont}{bold}{U}{txmia}{bx}{it}
+\DeclareMathSymbol{\bbbA}{\mathord}{bbbfont}{129}
+\DeclareMathSymbol{\bbbB}{\mathord}{bbbfont}{130}
+\DeclareMathSymbol{\bbbC}{\mathord}{bbbfont}{131}
+\DeclareMathSymbol{\bbbD}{\mathord}{bbbfont}{132}
+\DeclareMathSymbol{\bbbE}{\mathord}{bbbfont}{133}
+\DeclareMathSymbol{\bbbF}{\mathord}{bbbfont}{134}
+\DeclareMathSymbol{\bbbG}{\mathord}{bbbfont}{135}
+\DeclareMathSymbol{\bbbH}{\mathord}{bbbfont}{136}
+\DeclareMathSymbol{\bbbI}{\mathord}{bbbfont}{137}
+\DeclareMathSymbol{\bbbJ}{\mathord}{bbbfont}{138}
+\DeclareMathSymbol{\bbbK}{\mathord}{bbbfont}{139}
+\DeclareMathSymbol{\bbbL}{\mathord}{bbbfont}{140}
+\DeclareMathSymbol{\bbbM}{\mathord}{bbbfont}{141}
+\DeclareMathSymbol{\bbbN}{\mathord}{bbbfont}{142}
+\DeclareMathSymbol{\bbbO}{\mathord}{bbbfont}{143}
+\DeclareMathSymbol{\bbbP}{\mathord}{bbbfont}{144}
+\DeclareMathSymbol{\bbbQ}{\mathord}{bbbfont}{145}
+\DeclareMathSymbol{\bbbR}{\mathord}{bbbfont}{146}
+\DeclareMathSymbol{\bbbS}{\mathord}{bbbfont}{147}
+\DeclareMathSymbol{\bbbT}{\mathord}{bbbfont}{148}
+\DeclareMathSymbol{\bbbU}{\mathord}{bbbfont}{149}
+\DeclareMathSymbol{\bbbV}{\mathord}{bbbfont}{150}
+\DeclareMathSymbol{\bbbW}{\mathord}{bbbfont}{151}
+\DeclareMathSymbol{\bbbX}{\mathord}{bbbfont}{152}
+\DeclareMathSymbol{\bbbY}{\mathord}{bbbfont}{153}
+\DeclareMathSymbol{\bbbZ}{\mathord}{bbbfont}{154}
+
 \newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
 
 \newdimen\isa@parindent\newdimen\isa@parskip
@@ -112,8 +142,8 @@
 \chardef\isachartilde=`\~%
 \def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}%
 \def\isacharverbatimclose{\isacharasterisk\isacharbraceright}%
-\def\isacartoucheopen{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
-\def\isacartoucheclose{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
+\def\isacartoucheopen{\isatext{\guilsinglleft}}%
+\def\isacartoucheclose{\isatext{\guilsinglright}}%
 }
 
 
@@ -143,6 +173,12 @@
 \newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
 
 
+% index entries
+
+\newcommand{\isaindexdef}[1]{\textbf{#1}}
+\newcommand{\isaindexref}[1]{#1}
+
+
 % styles
 
 \def\isabellestyle#1{\csname isabellestyle#1\endcsname}
@@ -205,8 +241,8 @@
 \def\isacharbar{\isamath{\mid}}%
 \def\isacharbraceright{\isamath{\}}}%
 \def\isachartilde{\isamath{{}\sp{\sim}}}%
-\def\isacharbackquoteopen{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
-\def\isacharbackquoteclose{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
+\def\isacharbackquoteopen{\isatext{\guilsinglleft}}%
+\def\isacharbackquoteclose{\isatext{\guilsinglright}}%
 }
 
 \newcommand{\isabellestyleliteral}{%
@@ -239,29 +275,8 @@
 \newcommand{\isamarkupcancel}[1]{\isa{\xout{#1}}}
 
 
-% tagged regions
-
-%plain TeX version of comment package -- much faster!
-\let\isafmtname\fmtname\def\fmtname{plain}
-\usepackage{comment}
-\let\fmtname\isafmtname
+% tags
 
 \newcommand{\isafold}[1]{\emph{$\langle\mathord{\mathit{#1}}\rangle$}}
 
-\newcommand{\isakeeptag}[1]%
-{\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}}
-\newcommand{\isadroptag}[1]%
-{\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}}
-\newcommand{\isafoldtag}[1]%
-{\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}}
-
-\isakeeptag{document}
-\isakeeptag{theory}
-\isakeeptag{proof}
-\isakeeptag{ML}
-\isakeeptag{visible}
-\isadroptag{invisible}
-\isakeeptag{important}
-\isakeeptag{unimportant}
-
 \IfFileExists{isabelletags.sty}{\usepackage{isabelletags}}{}