doc-src/isabelle.sty
changeset 42511 bf89455ccf9d
parent 42510 b9c106763325
child 42512 f1ca2b0e0265
     1.1 --- a/doc-src/isabelle.sty	Sun May 01 00:01:59 2011 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,218 +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 -
    1.14 -\newcommand{\isastyle}{\UNDEF}
    1.15 -\newcommand{\isastyleminor}{\UNDEF}
    1.16 -\newcommand{\isastylescript}{\UNDEF}
    1.17 -\newcommand{\isastyletext}{\normalsize\rm}
    1.18 -\newcommand{\isastyletxt}{\rm}
    1.19 -\newcommand{\isastylecmt}{\rm}
    1.20 -
    1.21 -%symbol markup -- \emph achieves decent spacing via italic corrections
    1.22 -\newcommand{\isamath}[1]{\emph{$#1$}}
    1.23 -\newcommand{\isatext}[1]{\emph{#1}}
    1.24 -\DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
    1.25 -\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
    1.26 -\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
    1.27 -\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
    1.28 -\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
    1.29 -\DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isastylescript}
    1.30 -\DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup}
    1.31 -\DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isastylescript}
    1.32 -\DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}
    1.33 -\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
    1.34 -\newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}}
    1.35 -
    1.36 -\newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
    1.37 -\newcommand{\isaantiqopen}{\isakeyword{\isacharbraceleft}}
    1.38 -\newcommand{\isaantiqclose}{\isakeyword{\isacharbraceright}}
    1.39 -
    1.40 -\newdimen\isa@parindent\newdimen\isa@parskip
    1.41 -
    1.42 -\newenvironment{isabellebody}{%
    1.43 -\isamarkuptrue\par%
    1.44 -\isa@parindent\parindent\parindent0pt%
    1.45 -\isa@parskip\parskip\parskip0pt%
    1.46 -\isastyle}{\par}
    1.47 -
    1.48 -\newenvironment{isabelle}
    1.49 -{\begin{trivlist}\begin{isabellebody}\item\relax}
    1.50 -{\end{isabellebody}\end{trivlist}}
    1.51 -
    1.52 -\newcommand{\isa}[1]{\emph{\isastyleminor #1}}
    1.53 -
    1.54 -\newcommand{\isaindent}[1]{\hphantom{#1}}
    1.55 -\newcommand{\isanewline}{\mbox{}\par\mbox{}}
    1.56 -\newcommand{\isasep}{}
    1.57 -\newcommand{\isadigit}[1]{#1}
    1.58 -
    1.59 -\newcommand{\isachardefaults}{%
    1.60 -\chardef\isacharbang=`\!%
    1.61 -\chardef\isachardoublequote=`\"%
    1.62 -\chardef\isachardoublequoteopen=`\"%
    1.63 -\chardef\isachardoublequoteclose=`\"%
    1.64 -\chardef\isacharhash=`\#%
    1.65 -\chardef\isachardollar=`\$%
    1.66 -\chardef\isacharpercent=`\%%
    1.67 -\chardef\isacharampersand=`\&%
    1.68 -\chardef\isacharprime=`\'%
    1.69 -\chardef\isacharparenleft=`\(%
    1.70 -\chardef\isacharparenright=`\)%
    1.71 -\chardef\isacharasterisk=`\*%
    1.72 -\chardef\isacharplus=`\+%
    1.73 -\chardef\isacharcomma=`\,%
    1.74 -\chardef\isacharminus=`\-%
    1.75 -\chardef\isachardot=`\.%
    1.76 -\chardef\isacharslash=`\/%
    1.77 -\chardef\isacharcolon=`\:%
    1.78 -\chardef\isacharsemicolon=`\;%
    1.79 -\chardef\isacharless=`\<%
    1.80 -\chardef\isacharequal=`\=%
    1.81 -\chardef\isachargreater=`\>%
    1.82 -\chardef\isacharquery=`\?%
    1.83 -\chardef\isacharat=`\@%
    1.84 -\chardef\isacharbrackleft=`\[%
    1.85 -\chardef\isacharbackslash=`\\%
    1.86 -\chardef\isacharbrackright=`\]%
    1.87 -\chardef\isacharcircum=`\^%
    1.88 -\chardef\isacharunderscore=`\_%
    1.89 -\def\isacharunderscorekeyword{\_}%
    1.90 -\chardef\isacharbackquote=`\`%
    1.91 -\chardef\isacharbackquoteopen=`\`%
    1.92 -\chardef\isacharbackquoteclose=`\`%
    1.93 -\chardef\isacharbraceleft=`\{%
    1.94 -\chardef\isacharbar=`\|%
    1.95 -\chardef\isacharbraceright=`\}%
    1.96 -\chardef\isachartilde=`\~%
    1.97 -\def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}%
    1.98 -\def\isacharverbatimclose{\isacharasterisk\isacharbraceright}%
    1.99 -}
   1.100 -
   1.101 -\newcommand{\isaliteral}[2]{#2}
   1.102 -\newcommand{\isanil}{}
   1.103 -
   1.104 -
   1.105 -% keyword and section markup
   1.106 -
   1.107 -\newcommand{\isakeyword}[1]
   1.108 -{\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}%
   1.109 -\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
   1.110 -\newcommand{\isacommand}[1]{\isakeyword{#1}}
   1.111 -
   1.112 -\newcommand{\isamarkupheader}[1]{\section{#1}}
   1.113 -\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
   1.114 -\newcommand{\isamarkupsection}[1]{\section{#1}}
   1.115 -\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
   1.116 -\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
   1.117 -\newcommand{\isamarkupsect}[1]{\section{#1}}
   1.118 -\newcommand{\isamarkupsubsect}[1]{\subsection{#1}}
   1.119 -\newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
   1.120 -
   1.121 -\newif\ifisamarkup
   1.122 -\newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
   1.123 -\newcommand{\isaendpar}{\par\medskip}
   1.124 -\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
   1.125 -\newenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}}{\end{isapar}}
   1.126 -\newenvironment{isamarkuptxt}{\par\isastyletxt\begin{isapar}}{\end{isapar}}
   1.127 -\newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
   1.128 -
   1.129 -
   1.130 -% styles
   1.131 -
   1.132 -\def\isabellestyle#1{\csname isabellestyle#1\endcsname}
   1.133 -
   1.134 -\newcommand{\isabellestyledefault}{%
   1.135 -\renewcommand{\isastyle}{\small\tt\slshape}%
   1.136 -\renewcommand{\isastyleminor}{\small\tt\slshape}%
   1.137 -\renewcommand{\isastylescript}{\footnotesize\tt\slshape}%
   1.138 -\isachardefaults%
   1.139 -}
   1.140 -\isabellestyledefault
   1.141 -
   1.142 -\newcommand{\isabellestylett}{%
   1.143 -\renewcommand{\isastyle}{\small\tt}%
   1.144 -\renewcommand{\isastyleminor}{\small\tt}%
   1.145 -\renewcommand{\isastylescript}{\footnotesize\tt}%
   1.146 -\isachardefaults%
   1.147 -}
   1.148 -
   1.149 -\newcommand{\isabellestyleit}{%
   1.150 -\renewcommand{\isastyle}{\small\it}%
   1.151 -\renewcommand{\isastyleminor}{\it}%
   1.152 -\renewcommand{\isastylescript}{\footnotesize\it}%
   1.153 -\renewcommand{\isacharunderscorekeyword}{\mbox{-}}%
   1.154 -\renewcommand{\isacharbang}{\isamath{!}}%
   1.155 -\renewcommand{\isachardoublequote}{\isanil}%
   1.156 -\renewcommand{\isachardoublequoteopen}{\isanil}%
   1.157 -\renewcommand{\isachardoublequoteclose}{\isanil}%
   1.158 -\renewcommand{\isacharhash}{\isamath{\#}}%
   1.159 -\renewcommand{\isachardollar}{\isamath{\$}}%
   1.160 -\renewcommand{\isacharpercent}{\isamath{\%}}%
   1.161 -\renewcommand{\isacharampersand}{\isamath{\&}}%
   1.162 -\renewcommand{\isacharprime}{\isamath{\mskip2mu{'}\mskip-2mu}}%
   1.163 -\renewcommand{\isacharparenleft}{\isamath{(}}%
   1.164 -\renewcommand{\isacharparenright}{\isamath{)}}%
   1.165 -\renewcommand{\isacharasterisk}{\isamath{*}}%
   1.166 -\renewcommand{\isacharplus}{\isamath{+}}%
   1.167 -\renewcommand{\isacharcomma}{\isamath{\mathord,}}%
   1.168 -\renewcommand{\isacharminus}{\isamath{-}}%
   1.169 -\renewcommand{\isachardot}{\isamath{\mathord.}}%
   1.170 -\renewcommand{\isacharslash}{\isamath{/}}%
   1.171 -\renewcommand{\isacharcolon}{\isamath{\mathord:}}%
   1.172 -\renewcommand{\isacharsemicolon}{\isamath{\mathord;}}%
   1.173 -\renewcommand{\isacharless}{\isamath{<}}%
   1.174 -\renewcommand{\isacharequal}{\isamath{=}}%
   1.175 -\renewcommand{\isachargreater}{\isamath{>}}%
   1.176 -\renewcommand{\isacharat}{\isamath{@}}%
   1.177 -\renewcommand{\isacharbrackleft}{\isamath{[}}%
   1.178 -\renewcommand{\isacharbackslash}{\isamath{\backslash}}%
   1.179 -\renewcommand{\isacharbrackright}{\isamath{]}}%
   1.180 -\renewcommand{\isacharunderscore}{\mbox{-}}%
   1.181 -\renewcommand{\isacharbraceleft}{\isamath{\{}}%
   1.182 -\renewcommand{\isacharbar}{\isamath{\mid}}%
   1.183 -\renewcommand{\isacharbraceright}{\isamath{\}}}%
   1.184 -\renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}%
   1.185 -\renewcommand{\isacharbackquoteopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
   1.186 -\renewcommand{\isacharbackquoteclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
   1.187 -\renewcommand{\isacharverbatimopen}{\isamath{\langle\!\langle}}%
   1.188 -\renewcommand{\isacharverbatimclose}{\isamath{\rangle\!\rangle}}%
   1.189 -}
   1.190 -
   1.191 -\newcommand{\isabellestylesl}{%
   1.192 -\isabellestyleit%
   1.193 -\renewcommand{\isastyle}{\small\sl}%
   1.194 -\renewcommand{\isastyleminor}{\sl}%
   1.195 -\renewcommand{\isastylescript}{\footnotesize\sl}%
   1.196 -}
   1.197 -
   1.198 -
   1.199 -% tagged regions
   1.200 -
   1.201 -%plain TeX version of comment package -- much faster!
   1.202 -\let\isafmtname\fmtname\def\fmtname{plain}
   1.203 -\usepackage{comment}
   1.204 -\let\fmtname\isafmtname
   1.205 -
   1.206 -\newcommand{\isafold}[1]{\emph{$\langle\mathord{\mathit{#1}}\rangle$}}
   1.207 -
   1.208 -\newcommand{\isakeeptag}[1]%
   1.209 -{\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}}
   1.210 -\newcommand{\isadroptag}[1]%
   1.211 -{\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}}
   1.212 -\newcommand{\isafoldtag}[1]%
   1.213 -{\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}}
   1.214 -
   1.215 -\isakeeptag{theory}
   1.216 -\isakeeptag{proof}
   1.217 -\isakeeptag{ML}
   1.218 -\isakeeptag{visible}
   1.219 -\isadroptag{invisible}
   1.220 -
   1.221 -\IfFileExists{isabelletags.sty}{\usepackage{isabelletags}}{}