1.1 --- a/src/Tools/isac/Doc/isabelle.sty Thu Apr 08 13:09:44 2021 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,269 +0,0 @@
1.4 -%%
1.5 -%% macros for Isabelle generated LaTeX output
1.6 -%%
1.7 -
1.8 -%%% Simple document preparation (based on theory token language and symbols)
1.9 -
1.10 -% isabelle environments
1.11 -
1.12 -\newcommand{\isabellecontext}{UNKNOWN}
1.13 -\newcommand{\setisabellecontext}[1]{\def\isabellecontext{#1}}
1.14 -
1.15 -\newcommand{\isastyle}{\UNDEF}
1.16 -\newcommand{\isastylett}{\UNDEF}
1.17 -\newcommand{\isastyleminor}{\UNDEF}
1.18 -\newcommand{\isastyleminortt}{\UNDEF}
1.19 -\newcommand{\isastylescript}{\UNDEF}
1.20 -\newcommand{\isastyletext}{\normalsize\normalfont\rmfamily}
1.21 -\newcommand{\isastyletxt}{\normalfont\rmfamily}
1.22 -\newcommand{\isastylecmt}{\normalfont\rmfamily}
1.23 -
1.24 -\newcommand{\isaspacing}{%
1.25 - \sfcode 42 1000 % .
1.26 - \sfcode 63 1000 % ?
1.27 - \sfcode 33 1000 % !
1.28 - \sfcode 58 1000 % :
1.29 - \sfcode 59 1000 % ;
1.30 - \sfcode 44 1000 % ,
1.31 -}
1.32 -
1.33 -%symbol markup -- \emph achieves decent spacing via italic corrections
1.34 -\newcommand{\isamath}[1]{\emph{$#1$}}
1.35 -\newcommand{\isatext}[1]{\emph{#1}}
1.36 -\DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isaspacing\isastylescript##1}}}
1.37 -\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
1.38 -\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
1.39 -\DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isaspacing\isastylescript}
1.40 -\DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup}
1.41 -\DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isaspacing\isastylescript}
1.42 -\DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}
1.43 -\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
1.44 -
1.45 -\newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
1.46 -
1.47 -\newdimen\isa@parindent\newdimen\isa@parskip
1.48 -
1.49 -\newenvironment{isabellebody}{%
1.50 -\isamarkuptrue\par%
1.51 -\isa@parindent\parindent\parindent0pt%
1.52 -\isa@parskip\parskip\parskip0pt%
1.53 -\isaspacing\isastyle}{\par}
1.54 -
1.55 -\newenvironment{isabellebodytt}{%
1.56 -\isamarkuptrue\par%
1.57 -\isa@parindent\parindent\parindent0pt%
1.58 -\isa@parskip\parskip\parskip0pt%
1.59 -\isaspacing\isastylett}{\par}
1.60 -
1.61 -\newenvironment{isabelle}
1.62 -{\begin{trivlist}\begin{isabellebody}\item\relax}
1.63 -{\end{isabellebody}\end{trivlist}}
1.64 -
1.65 -\newenvironment{isabellett}
1.66 -{\begin{trivlist}\begin{isabellebodytt}\item\relax}
1.67 -{\end{isabellebodytt}\end{trivlist}}
1.68 -
1.69 -\newcommand{\isa}[1]{\emph{\isaspacing\isastyleminor #1}}
1.70 -\newcommand{\isatt}[1]{\emph{\isaspacing\isastyleminortt #1}}
1.71 -
1.72 -\newcommand{\isaindent}[1]{\hphantom{#1}}
1.73 -\newcommand{\isanewline}{\mbox{}\par\mbox{}}
1.74 -\newcommand{\isasep}{}
1.75 -\newcommand{\isadigit}[1]{#1}
1.76 -
1.77 -\newcommand{\isachardefaults}{%
1.78 -\def\isacharbell{\isamath{\bigbox}}%requires stmaryrd
1.79 -\chardef\isacharbang=`\!%
1.80 -\chardef\isachardoublequote=`\"%
1.81 -\chardef\isachardoublequoteopen=`\"%
1.82 -\chardef\isachardoublequoteclose=`\"%
1.83 -\chardef\isacharhash=`\#%
1.84 -\chardef\isachardollar=`\$%
1.85 -\chardef\isacharpercent=`\%%
1.86 -\chardef\isacharampersand=`\&%
1.87 -\chardef\isacharprime=`\'%
1.88 -\chardef\isacharparenleft=`\(%
1.89 -\chardef\isacharparenright=`\)%
1.90 -\chardef\isacharasterisk=`\*%
1.91 -\chardef\isacharplus=`\+%
1.92 -\chardef\isacharcomma=`\,%
1.93 -\chardef\isacharminus=`\-%
1.94 -\chardef\isachardot=`\.%
1.95 -\chardef\isacharslash=`\/%
1.96 -\chardef\isacharcolon=`\:%
1.97 -\chardef\isacharsemicolon=`\;%
1.98 -\chardef\isacharless=`\<%
1.99 -\chardef\isacharequal=`\=%
1.100 -\chardef\isachargreater=`\>%
1.101 -\chardef\isacharquery=`\?%
1.102 -\chardef\isacharat=`\@%
1.103 -\chardef\isacharbrackleft=`\[%
1.104 -\chardef\isacharbackslash=`\\%
1.105 -\chardef\isacharbrackright=`\]%
1.106 -\chardef\isacharcircum=`\^%
1.107 -\chardef\isacharunderscore=`\_%
1.108 -\def\isacharunderscorekeyword{\_}%
1.109 -\chardef\isacharbackquote=`\`%
1.110 -\chardef\isacharbackquoteopen=`\`%
1.111 -\chardef\isacharbackquoteclose=`\`%
1.112 -\chardef\isacharbraceleft=`\{%
1.113 -\chardef\isacharbar=`\|%
1.114 -\chardef\isacharbraceright=`\}%
1.115 -\chardef\isachartilde=`\~%
1.116 -\def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}%
1.117 -\def\isacharverbatimclose{\isacharasterisk\isacharbraceright}%
1.118 -\def\isacartoucheopen{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
1.119 -\def\isacartoucheclose{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
1.120 -}
1.121 -
1.122 -
1.123 -% keyword and section markup
1.124 -
1.125 -\newcommand{\isakeyword}[1]
1.126 -{\emph{\normalfont\bfseries\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}%
1.127 -\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
1.128 -\newcommand{\isacommand}[1]{\isakeyword{#1}}
1.129 -
1.130 -\newcommand{\isakeywordcontrol}[1]
1.131 -{\emph{\normalfont\bfseries\itshape\def\isacharunderscore{\isacharunderscorekeyword}#1\,}}
1.132 -
1.133 -\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
1.134 -\newcommand{\isamarkupsection}[1]{\section{#1}}
1.135 -\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
1.136 -\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
1.137 -\newcommand{\isamarkupparagraph}[1]{\paragraph{#1}}
1.138 -\newcommand{\isamarkupsubparagraph}[1]{\subparagraph{#1}}
1.139 -
1.140 -\newif\ifisamarkup
1.141 -\newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
1.142 -\newcommand{\isaendpar}{\par\medskip}
1.143 -\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
1.144 -\newenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}}{\end{isapar}}
1.145 -\newenvironment{isamarkuptxt}{\par\isastyletxt\begin{isapar}}{\end{isapar}}
1.146 -\newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
1.147 -
1.148 -
1.149 -% styles
1.150 -
1.151 -\def\isabellestyle#1{\csname isabellestyle#1\endcsname}
1.152 -
1.153 -\newcommand{\isabellestyledefault}{%
1.154 -\def\isastyle{\small\normalfont\ttfamily\slshape}%
1.155 -\def\isastylett{\small\normalfont\ttfamily}%
1.156 -\def\isastyleminor{\small\normalfont\ttfamily\slshape}%
1.157 -\def\isastyleminortt{\small\normalfont\ttfamily}%
1.158 -\def\isastylescript{\footnotesize\normalfont\ttfamily\slshape}%
1.159 -\isachardefaults%
1.160 -}
1.161 -\isabellestyledefault
1.162 -
1.163 -\newcommand{\isabellestylett}{%
1.164 -\def\isastyle{\small\normalfont\ttfamily}%
1.165 -\def\isastylett{\small\normalfont\ttfamily}%
1.166 -\def\isastyleminor{\small\normalfont\ttfamily}%
1.167 -\def\isastyleminortt{\small\normalfont\ttfamily}%
1.168 -\def\isastylescript{\footnotesize\normalfont\ttfamily}%
1.169 -\isachardefaults%
1.170 -}
1.171 -
1.172 -\newcommand{\isabellestyleit}{%
1.173 -\def\isastyle{\small\normalfont\itshape}%
1.174 -\def\isastylett{\small\normalfont\ttfamily}%
1.175 -\def\isastyleminor{\normalfont\itshape}%
1.176 -\def\isastyleminortt{\normalfont\ttfamily}%
1.177 -\def\isastylescript{\footnotesize\normalfont\itshape}%
1.178 -\isachardefaults%
1.179 -\def\isacharunderscorekeyword{\mbox{-}}%
1.180 -\def\isacharbang{\isamath{!}}%
1.181 -\def\isachardoublequote{}%
1.182 -\def\isachardoublequoteopen{}%
1.183 -\def\isachardoublequoteclose{}%
1.184 -\def\isacharhash{\isamath{\#}}%
1.185 -\def\isachardollar{\isamath{\$}}%
1.186 -\def\isacharpercent{\isamath{\%}}%
1.187 -\def\isacharampersand{\isamath{\&}}%
1.188 -\def\isacharprime{\isamath{\mskip2mu{'}\mskip-2mu}}%
1.189 -\def\isacharparenleft{\isamath{(}}%
1.190 -\def\isacharparenright{\isamath{)}}%
1.191 -\def\isacharasterisk{\isamath{*}}%
1.192 -\def\isacharplus{\isamath{+}}%
1.193 -\def\isacharcomma{\isamath{\mathord,}}%
1.194 -\def\isacharminus{\isamath{-}}%
1.195 -\def\isachardot{\isamath{\mathord.}}%
1.196 -\def\isacharslash{\isamath{/}}%
1.197 -\def\isacharcolon{\isamath{\mathord:}}%
1.198 -\def\isacharsemicolon{\isamath{\mathord;}}%
1.199 -\def\isacharless{\isamath{<}}%
1.200 -\def\isacharequal{\isamath{=}}%
1.201 -\def\isachargreater{\isamath{>}}%
1.202 -\def\isacharat{\isamath{@}}%
1.203 -\def\isacharbrackleft{\isamath{[}}%
1.204 -\def\isacharbackslash{\isamath{\backslash}}%
1.205 -\def\isacharbrackright{\isamath{]}}%
1.206 -\def\isacharunderscore{\mbox{-}}%
1.207 -\def\isacharbraceleft{\isamath{\{}}%
1.208 -\def\isacharbar{\isamath{\mid}}%
1.209 -\def\isacharbraceright{\isamath{\}}}%
1.210 -\def\isachartilde{\isamath{{}\sp{\sim}}}%
1.211 -\def\isacharbackquoteopen{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
1.212 -\def\isacharbackquoteclose{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
1.213 -\def\isacharverbatimopen{\isamath{\langle\!\langle}}%
1.214 -\def\isacharverbatimclose{\isamath{\rangle\!\rangle}}%
1.215 -}
1.216 -
1.217 -\newcommand{\isabellestyleliteral}{%
1.218 -\isabellestyleit%
1.219 -\def\isacharunderscore{\_}%
1.220 -\def\isacharunderscorekeyword{\_}%
1.221 -\chardef\isacharbackquoteopen=`\`%
1.222 -\chardef\isacharbackquoteclose=`\`%
1.223 -}
1.224 -
1.225 -\newcommand{\isabellestyleliteralunderscore}{%
1.226 -\isabellestyleliteral%
1.227 -\def\isacharunderscore{\textunderscore}%
1.228 -\def\isacharunderscorekeyword{\textunderscore}%
1.229 -}
1.230 -
1.231 -\newcommand{\isabellestylesl}{%
1.232 -\isabellestyleit%
1.233 -\def\isastyle{\small\normalfont\slshape}%
1.234 -\def\isastylett{\small\normalfont\ttfamily}%
1.235 -\def\isastyleminor{\normalfont\slshape}%
1.236 -\def\isastyleminortt{\normalfont\ttfamily}%
1.237 -\def\isastylescript{\footnotesize\normalfont\slshape}%
1.238 -}
1.239 -
1.240 -
1.241 -% cancel text
1.242 -
1.243 -\usepackage[normalem]{ulem}
1.244 -\newcommand{\isamarkupcancel}[1]{\isa{\xout{#1}}}
1.245 -
1.246 -
1.247 -% tagged regions
1.248 -
1.249 -%plain TeX version of comment package -- much faster!
1.250 -\let\isafmtname\fmtname\def\fmtname{plain}
1.251 -\usepackage{comment}
1.252 -\let\fmtname\isafmtname
1.253 -
1.254 -\newcommand{\isafold}[1]{\emph{$\langle\mathord{\mathit{#1}}\rangle$}}
1.255 -
1.256 -\newcommand{\isakeeptag}[1]%
1.257 -{\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}}
1.258 -\newcommand{\isadroptag}[1]%
1.259 -{\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}}
1.260 -\newcommand{\isafoldtag}[1]%
1.261 -{\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}}
1.262 -
1.263 -\isakeeptag{document}
1.264 -\isakeeptag{theory}
1.265 -\isakeeptag{proof}
1.266 -\isakeeptag{ML}
1.267 -\isakeeptag{visible}
1.268 -\isadroptag{invisible}
1.269 -\isakeeptag{important}
1.270 -\isakeeptag{unimportant}
1.271 -
1.272 -\IfFileExists{isabelletags.sty}{\usepackage{isabelletags}}{}