diff -r 751b8a13c271 -r 422186a35be8 src/Tools/isac/Doc/isabelle.sty
--- a/src/Tools/isac/Doc/isabelle.sty	Thu Apr 08 13:09:44 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,269 +0,0 @@
-%%
-%% macros for Isabelle generated LaTeX output
-%%
-
-%%% Simple document preparation (based on theory token language and symbols)
-
-% isabelle environments
-
-\newcommand{\isabellecontext}{UNKNOWN}
-\newcommand{\setisabellecontext}[1]{\def\isabellecontext{#1}}
-
-\newcommand{\isastyle}{\UNDEF}
-\newcommand{\isastylett}{\UNDEF}
-\newcommand{\isastyleminor}{\UNDEF}
-\newcommand{\isastyleminortt}{\UNDEF}
-\newcommand{\isastylescript}{\UNDEF}
-\newcommand{\isastyletext}{\normalsize\normalfont\rmfamily}
-\newcommand{\isastyletxt}{\normalfont\rmfamily}
-\newcommand{\isastylecmt}{\normalfont\rmfamily}
-
-\newcommand{\isaspacing}{%
-  \sfcode 42 1000 % .
-  \sfcode 63 1000 % ?
-  \sfcode 33 1000 % !
-  \sfcode 58 1000 % :
-  \sfcode 59 1000 % ;
-  \sfcode 44 1000 % ,
-}
-
-%symbol markup -- \emph achieves decent spacing via italic corrections
-\newcommand{\isamath}[1]{\emph{$#1$}}
-\newcommand{\isatext}[1]{\emph{#1}}
-\DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isaspacing\isastylescript##1}}}
-\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
-\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
-\DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isaspacing\isastylescript}
-\DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup}
-\DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isaspacing\isastylescript}
-\DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}
-\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
-
-\newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
-
-\newdimen\isa@parindent\newdimen\isa@parskip
-
-\newenvironment{isabellebody}{%
-\isamarkuptrue\par%
-\isa@parindent\parindent\parindent0pt%
-\isa@parskip\parskip\parskip0pt%
-\isaspacing\isastyle}{\par}
-
-\newenvironment{isabellebodytt}{%
-\isamarkuptrue\par%
-\isa@parindent\parindent\parindent0pt%
-\isa@parskip\parskip\parskip0pt%
-\isaspacing\isastylett}{\par}
-
-\newenvironment{isabelle}
-{\begin{trivlist}\begin{isabellebody}\item\relax}
-{\end{isabellebody}\end{trivlist}}
-
-\newenvironment{isabellett}
-{\begin{trivlist}\begin{isabellebodytt}\item\relax}
-{\end{isabellebodytt}\end{trivlist}}
-
-\newcommand{\isa}[1]{\emph{\isaspacing\isastyleminor #1}}
-\newcommand{\isatt}[1]{\emph{\isaspacing\isastyleminortt #1}}
-
-\newcommand{\isaindent}[1]{\hphantom{#1}}
-\newcommand{\isanewline}{\mbox{}\par\mbox{}}
-\newcommand{\isasep}{}
-\newcommand{\isadigit}[1]{#1}
-
-\newcommand{\isachardefaults}{%
-\def\isacharbell{\isamath{\bigbox}}%requires stmaryrd
-\chardef\isacharbang=`\!%
-\chardef\isachardoublequote=`\"%
-\chardef\isachardoublequoteopen=`\"%
-\chardef\isachardoublequoteclose=`\"%
-\chardef\isacharhash=`\#%
-\chardef\isachardollar=`\$%
-\chardef\isacharpercent=`\%%
-\chardef\isacharampersand=`\&%
-\chardef\isacharprime=`\'%
-\chardef\isacharparenleft=`\(%
-\chardef\isacharparenright=`\)%
-\chardef\isacharasterisk=`\*%
-\chardef\isacharplus=`\+%
-\chardef\isacharcomma=`\,%
-\chardef\isacharminus=`\-%
-\chardef\isachardot=`\.%
-\chardef\isacharslash=`\/%
-\chardef\isacharcolon=`\:%
-\chardef\isacharsemicolon=`\;%
-\chardef\isacharless=`\<%
-\chardef\isacharequal=`\=%
-\chardef\isachargreater=`\>%
-\chardef\isacharquery=`\?%
-\chardef\isacharat=`\@%
-\chardef\isacharbrackleft=`\[%
-\chardef\isacharbackslash=`\\%
-\chardef\isacharbrackright=`\]%
-\chardef\isacharcircum=`\^%
-\chardef\isacharunderscore=`\_%
-\def\isacharunderscorekeyword{\_}%
-\chardef\isacharbackquote=`\`%
-\chardef\isacharbackquoteopen=`\`%
-\chardef\isacharbackquoteclose=`\`%
-\chardef\isacharbraceleft=`\{%
-\chardef\isacharbar=`\|%
-\chardef\isacharbraceright=`\}%
-\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$}}}%
-}
-
-
-% keyword and section markup
-
-\newcommand{\isakeyword}[1]
-{\emph{\normalfont\bfseries\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}%
-\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
-\newcommand{\isacommand}[1]{\isakeyword{#1}}
-
-\newcommand{\isakeywordcontrol}[1]
-{\emph{\normalfont\bfseries\itshape\def\isacharunderscore{\isacharunderscorekeyword}#1\,}}
-
-\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
-\newcommand{\isamarkupsection}[1]{\section{#1}}
-\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
-\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
-\newcommand{\isamarkupparagraph}[1]{\paragraph{#1}}
-\newcommand{\isamarkupsubparagraph}[1]{\subparagraph{#1}}
-
-\newif\ifisamarkup
-\newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
-\newcommand{\isaendpar}{\par\medskip}
-\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
-\newenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}}{\end{isapar}}
-\newenvironment{isamarkuptxt}{\par\isastyletxt\begin{isapar}}{\end{isapar}}
-\newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
-
-
-% styles
-
-\def\isabellestyle#1{\csname isabellestyle#1\endcsname}
-
-\newcommand{\isabellestyledefault}{%
-\def\isastyle{\small\normalfont\ttfamily\slshape}%
-\def\isastylett{\small\normalfont\ttfamily}%
-\def\isastyleminor{\small\normalfont\ttfamily\slshape}%
-\def\isastyleminortt{\small\normalfont\ttfamily}%
-\def\isastylescript{\footnotesize\normalfont\ttfamily\slshape}%
-\isachardefaults%
-}
-\isabellestyledefault
-
-\newcommand{\isabellestylett}{%
-\def\isastyle{\small\normalfont\ttfamily}%
-\def\isastylett{\small\normalfont\ttfamily}%
-\def\isastyleminor{\small\normalfont\ttfamily}%
-\def\isastyleminortt{\small\normalfont\ttfamily}%
-\def\isastylescript{\footnotesize\normalfont\ttfamily}%
-\isachardefaults%
-}
-
-\newcommand{\isabellestyleit}{%
-\def\isastyle{\small\normalfont\itshape}%
-\def\isastylett{\small\normalfont\ttfamily}%
-\def\isastyleminor{\normalfont\itshape}%
-\def\isastyleminortt{\normalfont\ttfamily}%
-\def\isastylescript{\footnotesize\normalfont\itshape}%
-\isachardefaults%
-\def\isacharunderscorekeyword{\mbox{-}}%
-\def\isacharbang{\isamath{!}}%
-\def\isachardoublequote{}%
-\def\isachardoublequoteopen{}%
-\def\isachardoublequoteclose{}%
-\def\isacharhash{\isamath{\#}}%
-\def\isachardollar{\isamath{\$}}%
-\def\isacharpercent{\isamath{\%}}%
-\def\isacharampersand{\isamath{\&}}%
-\def\isacharprime{\isamath{\mskip2mu{'}\mskip-2mu}}%
-\def\isacharparenleft{\isamath{(}}%
-\def\isacharparenright{\isamath{)}}%
-\def\isacharasterisk{\isamath{*}}%
-\def\isacharplus{\isamath{+}}%
-\def\isacharcomma{\isamath{\mathord,}}%
-\def\isacharminus{\isamath{-}}%
-\def\isachardot{\isamath{\mathord.}}%
-\def\isacharslash{\isamath{/}}%
-\def\isacharcolon{\isamath{\mathord:}}%
-\def\isacharsemicolon{\isamath{\mathord;}}%
-\def\isacharless{\isamath{<}}%
-\def\isacharequal{\isamath{=}}%
-\def\isachargreater{\isamath{>}}%
-\def\isacharat{\isamath{@}}%
-\def\isacharbrackleft{\isamath{[}}%
-\def\isacharbackslash{\isamath{\backslash}}%
-\def\isacharbrackright{\isamath{]}}%
-\def\isacharunderscore{\mbox{-}}%
-\def\isacharbraceleft{\isamath{\{}}%
-\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\isacharverbatimopen{\isamath{\langle\!\langle}}%
-\def\isacharverbatimclose{\isamath{\rangle\!\rangle}}%
-}
-
-\newcommand{\isabellestyleliteral}{%
-\isabellestyleit%
-\def\isacharunderscore{\_}%
-\def\isacharunderscorekeyword{\_}%
-\chardef\isacharbackquoteopen=`\`%
-\chardef\isacharbackquoteclose=`\`%
-}
-
-\newcommand{\isabellestyleliteralunderscore}{%
-\isabellestyleliteral%
-\def\isacharunderscore{\textunderscore}%
-\def\isacharunderscorekeyword{\textunderscore}%
-}
-
-\newcommand{\isabellestylesl}{%
-\isabellestyleit%
-\def\isastyle{\small\normalfont\slshape}%
-\def\isastylett{\small\normalfont\ttfamily}%
-\def\isastyleminor{\normalfont\slshape}%
-\def\isastyleminortt{\normalfont\ttfamily}%
-\def\isastylescript{\footnotesize\normalfont\slshape}%
-}
-
-
-% cancel text
-
-\usepackage[normalem]{ulem}
-\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
-
-\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}}{}