1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/isabelle.sty Thu May 15 20:14:10 2008 +0200
1.3 @@ -0,0 +1,215 @@
1.4 +%%
1.5 +%%
1.6 +%%
1.7 +%% macros for Isabelle generated LaTeX output
1.8 +%%
1.9 +
1.10 +%%% Simple document preparation (based on theory token language and symbols)
1.11 +
1.12 +% isabelle environments
1.13 +
1.14 +\newcommand{\isabellecontext}{UNKNOWN}
1.15 +
1.16 +\newcommand{\isastyle}{\UNDEF}
1.17 +\newcommand{\isastyleminor}{\UNDEF}
1.18 +\newcommand{\isastylescript}{\UNDEF}
1.19 +\newcommand{\isastyletext}{\normalsize\rm}
1.20 +\newcommand{\isastyletxt}{\rm}
1.21 +\newcommand{\isastylecmt}{\rm}
1.22 +
1.23 +%symbol markup -- \emph achieves decent spacing via italic corrections
1.24 +\newcommand{\isamath}[1]{\emph{$#1$}}
1.25 +\newcommand{\isatext}[1]{\emph{#1}}
1.26 +\DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
1.27 +\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
1.28 +\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
1.29 +\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
1.30 +\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
1.31 +\DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isastylescript}
1.32 +\DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup}
1.33 +\DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isastylescript}
1.34 +\DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}
1.35 +\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
1.36 +\newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}}
1.37 +\newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
1.38 +
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 +
1.102 +% keyword and section markup
1.103 +
1.104 +\newcommand{\isakeyword}[1]
1.105 +{\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}%
1.106 +\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
1.107 +\newcommand{\isacommand}[1]{\isakeyword{#1}}
1.108 +
1.109 +\newcommand{\isamarkupheader}[1]{\section{#1}}
1.110 +\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
1.111 +\newcommand{\isamarkupsection}[1]{\section{#1}}
1.112 +\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
1.113 +\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
1.114 +\newcommand{\isamarkupsect}[1]{\section{#1}}
1.115 +\newcommand{\isamarkupsubsect}[1]{\subsection{#1}}
1.116 +\newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
1.117 +
1.118 +\newif\ifisamarkup
1.119 +\newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
1.120 +\newcommand{\isaendpar}{\par\medskip}
1.121 +\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
1.122 +\newenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}}{\end{isapar}}
1.123 +\newenvironment{isamarkuptxt}{\par\isastyletxt\begin{isapar}}{\end{isapar}}
1.124 +\newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
1.125 +
1.126 +
1.127 +% styles
1.128 +
1.129 +\def\isabellestyle#1{\csname isabellestyle#1\endcsname}
1.130 +
1.131 +\newcommand{\isabellestyledefault}{%
1.132 +\renewcommand{\isastyle}{\small\tt\slshape}%
1.133 +\renewcommand{\isastyleminor}{\small\tt\slshape}%
1.134 +\renewcommand{\isastylescript}{\footnotesize\tt\slshape}%
1.135 +\isachardefaults%
1.136 +}
1.137 +\isabellestyledefault
1.138 +
1.139 +\newcommand{\isabellestylett}{%
1.140 +\renewcommand{\isastyle}{\small\tt}%
1.141 +\renewcommand{\isastyleminor}{\small\tt}%
1.142 +\renewcommand{\isastylescript}{\footnotesize\tt}%
1.143 +\isachardefaults%
1.144 +}
1.145 +
1.146 +\newcommand{\isabellestyleit}{%
1.147 +\renewcommand{\isastyle}{\small\it}%
1.148 +\renewcommand{\isastyleminor}{\it}%
1.149 +\renewcommand{\isastylescript}{\footnotesize\it}%
1.150 +\renewcommand{\isacharunderscorekeyword}{\mbox{-}}%
1.151 +\renewcommand{\isacharbang}{\isamath{!}}%
1.152 +\renewcommand{\isachardoublequote}{}%
1.153 +\renewcommand{\isachardoublequoteopen}{}%
1.154 +\renewcommand{\isachardoublequoteclose}{}%
1.155 +\renewcommand{\isacharhash}{\isamath{\#}}%
1.156 +\renewcommand{\isachardollar}{\isamath{\$}}%
1.157 +\renewcommand{\isacharpercent}{\isamath{\%}}%
1.158 +\renewcommand{\isacharampersand}{\isamath{\&}}%
1.159 +\renewcommand{\isacharprime}{\isamath{\mskip2mu{'}\mskip-2mu}}%
1.160 +\renewcommand{\isacharparenleft}{\isamath{(}}%
1.161 +\renewcommand{\isacharparenright}{\isamath{)}}%
1.162 +\renewcommand{\isacharasterisk}{\isamath{*}}%
1.163 +\renewcommand{\isacharplus}{\isamath{+}}%
1.164 +\renewcommand{\isacharcomma}{\isamath{\mathord,}}%
1.165 +\renewcommand{\isacharminus}{\isamath{-}}%
1.166 +\renewcommand{\isachardot}{\isamath{\mathord.}}%
1.167 +\renewcommand{\isacharslash}{\isamath{/}}%
1.168 +\renewcommand{\isacharcolon}{\isamath{\mathord:}}%
1.169 +\renewcommand{\isacharsemicolon}{\isamath{\mathord;}}%
1.170 +\renewcommand{\isacharless}{\isamath{<}}%
1.171 +\renewcommand{\isacharequal}{\isamath{=}}%
1.172 +\renewcommand{\isachargreater}{\isamath{>}}%
1.173 +\renewcommand{\isacharat}{\isamath{@}}%
1.174 +\renewcommand{\isacharbrackleft}{\isamath{[}}%
1.175 +\renewcommand{\isacharbackslash}{\isamath{\backslash}}%
1.176 +\renewcommand{\isacharbrackright}{\isamath{]}}%
1.177 +\renewcommand{\isacharunderscore}{\mbox{-}}%
1.178 +\renewcommand{\isacharbraceleft}{\isamath{\{}}%
1.179 +\renewcommand{\isacharbar}{\isamath{\mid}}%
1.180 +\renewcommand{\isacharbraceright}{\isamath{\}}}%
1.181 +\renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}%
1.182 +\renewcommand{\isacharbackquoteopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
1.183 +\renewcommand{\isacharbackquoteclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
1.184 +\renewcommand{\isacharverbatimopen}{\isamath{\langle\!\langle}}%
1.185 +\renewcommand{\isacharverbatimclose}{\isamath{\rangle\!\rangle}}%
1.186 +}
1.187 +
1.188 +\newcommand{\isabellestylesl}{%
1.189 +\isabellestyleit%
1.190 +\renewcommand{\isastyle}{\small\sl}%
1.191 +\renewcommand{\isastyleminor}{\sl}%
1.192 +\renewcommand{\isastylescript}{\footnotesize\sl}%
1.193 +}
1.194 +
1.195 +
1.196 +% tagged regions
1.197 +
1.198 +%plain TeX version of comment package -- much faster!
1.199 +\let\isafmtname\fmtname\def\fmtname{plain}
1.200 +\usepackage{comment}
1.201 +\let\fmtname\isafmtname
1.202 +
1.203 +\newcommand{\isafold}[1]{\emph{$\langle\mathord{\mathit{#1}}\rangle$}}
1.204 +
1.205 +\newcommand{\isakeeptag}[1]%
1.206 +{\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}}
1.207 +\newcommand{\isadroptag}[1]%
1.208 +{\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}}
1.209 +\newcommand{\isafoldtag}[1]%
1.210 +{\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}}
1.211 +
1.212 +\isakeeptag{theory}
1.213 +\isakeeptag{proof}
1.214 +\isakeeptag{ML}
1.215 +\isakeeptag{visible}
1.216 +\isadroptag{invisible}
1.217 +
1.218 +\IfFileExists{isabelletags.sty}{\usepackage{isabelletags}}{}