1.1 --- a/src/Doc/isac/jrocnik/isabelle.sty Mon Sep 16 12:27:20 2013 +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}}{}