diff -r 56781ad291cf -r e00950ba4514 thys2/Journal/isabelle.sty
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys2/Journal/isabelle.sty	Mon Nov 01 10:40:21 2021 +0000
@@ -0,0 +1,267 @@
+%%
+%% 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$}}}%
+}
+
+\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}}{}