1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/ZF/isabelle.sty Tue Aug 19 13:53:58 2003 +0200
1.3 @@ -0,0 +1,157 @@
1.4 +%%
1.5 +%% Author: Markus Wenzel, TU Muenchen
1.6 +%% License: GPL (GNU GENERAL PUBLIC LICENSE)
1.7 +%%
1.8 +%% macros for Isabelle generated LaTeX output
1.9 +%%
1.10 +
1.11 +%%% Simple document preparation (based on theory token language and symbols)
1.12 +
1.13 +% isabelle environments
1.14 +
1.15 +\newcommand{\isabellecontext}{UNKNOWN}
1.16 +
1.17 +\newcommand{\isastyle}{\small\tt\slshape}
1.18 +\newcommand{\isastyleminor}{\small\tt\slshape}
1.19 +\newcommand{\isastylescript}{\footnotesize\tt\slshape}
1.20 +\newcommand{\isastyletext}{\normalsize\rm}
1.21 +\newcommand{\isastyletxt}{\rm}
1.22 +\newcommand{\isastylecmt}{\rm}
1.23 +
1.24 +%symbol markup -- \emph achieves decent spacing via italic corrections
1.25 +\newcommand{\isamath}[1]{\emph{$#1$}}
1.26 +\newcommand{\isatext}[1]{\emph{#1}}
1.27 +\newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
1.28 +\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
1.29 +\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
1.30 +\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
1.31 +
1.32 +\newdimen\isa@parindent\newdimen\isa@parskip
1.33 +
1.34 +\newenvironment{isabellebody}{%
1.35 +\isamarkuptrue\par%
1.36 +\isa@parindent\parindent\parindent0pt%
1.37 +\isa@parskip\parskip\parskip0pt%
1.38 +\isastyle}{\par}
1.39 +
1.40 +\newenvironment{isabelle}
1.41 +{\begin{trivlist}\begin{isabellebody}\item\relax}
1.42 +{\end{isabellebody}\end{trivlist}}
1.43 +
1.44 +\newcommand{\isa}[1]{\emph{\isastyleminor #1}}
1.45 +
1.46 +\newcommand{\isaindent}[1]{\hphantom{#1}}
1.47 +\newcommand{\isanewline}{\mbox{}\par\mbox{}}
1.48 +\newcommand{\isadigit}[1]{#1}
1.49 +
1.50 +\chardef\isacharbang=`\!
1.51 +\chardef\isachardoublequote=`\"
1.52 +\chardef\isacharhash=`\#
1.53 +\chardef\isachardollar=`\$
1.54 +\chardef\isacharpercent=`\%
1.55 +\chardef\isacharampersand=`\&
1.56 +\chardef\isacharprime=`\'
1.57 +\chardef\isacharparenleft=`\(
1.58 +\chardef\isacharparenright=`\)
1.59 +\chardef\isacharasterisk=`\*
1.60 +\chardef\isacharplus=`\+
1.61 +\chardef\isacharcomma=`\,
1.62 +\chardef\isacharminus=`\-
1.63 +\chardef\isachardot=`\.
1.64 +\chardef\isacharslash=`\/
1.65 +\chardef\isacharcolon=`\:
1.66 +\chardef\isacharsemicolon=`\;
1.67 +\chardef\isacharless=`\<
1.68 +\chardef\isacharequal=`\=
1.69 +\chardef\isachargreater=`\>
1.70 +\chardef\isacharquery=`\?
1.71 +\chardef\isacharat=`\@
1.72 +\chardef\isacharbrackleft=`\[
1.73 +\chardef\isacharbackslash=`\\
1.74 +\chardef\isacharbrackright=`\]
1.75 +\chardef\isacharcircum=`\^
1.76 +\chardef\isacharunderscore=`\_
1.77 +\chardef\isacharbackquote=`\`
1.78 +\chardef\isacharbraceleft=`\{
1.79 +\chardef\isacharbar=`\|
1.80 +\chardef\isacharbraceright=`\}
1.81 +\chardef\isachartilde=`\~
1.82 +
1.83 +
1.84 +% keyword and section markup
1.85 +
1.86 +\newcommand{\isakeywordcharunderscore}{\_}
1.87 +\newcommand{\isakeyword}[1]
1.88 +{\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isakeywordcharunderscore}%
1.89 +\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
1.90 +\newcommand{\isacommand}[1]{\isakeyword{#1}}
1.91 +
1.92 +\newcommand{\isamarkupheader}[1]{\section{#1}}
1.93 +\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
1.94 +\newcommand{\isamarkupsection}[1]{\section{#1}}
1.95 +\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
1.96 +\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
1.97 +\newcommand{\isamarkupsect}[1]{\section{#1}}
1.98 +\newcommand{\isamarkupsubsect}[1]{\subsection{#1}}
1.99 +\newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
1.100 +
1.101 +\newif\ifisamarkup
1.102 +\newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
1.103 +\newcommand{\isaendpar}{\par\medskip}
1.104 +\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
1.105 +\newenvironment{isamarkuptext}{\isastyletext\begin{isapar}}{\end{isapar}}
1.106 +\newenvironment{isamarkuptxt}{\isastyletxt\begin{isapar}}{\end{isapar}}
1.107 +\newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
1.108 +
1.109 +
1.110 +% alternative styles
1.111 +
1.112 +\newcommand{\isabellestyle}{}
1.113 +\def\isabellestyle#1{\csname isabellestyle#1\endcsname}
1.114 +
1.115 +\newcommand{\isabellestylett}{%
1.116 +\renewcommand{\isastyle}{\small\tt}%
1.117 +\renewcommand{\isastyleminor}{\small\tt}%
1.118 +\renewcommand{\isastylescript}{\footnotesize\tt}%
1.119 +}
1.120 +\newcommand{\isabellestyleit}{%
1.121 +\renewcommand{\isastyle}{\small\it}%
1.122 +\renewcommand{\isastyleminor}{\it}%
1.123 +\renewcommand{\isastylescript}{\footnotesize\it}%
1.124 +\renewcommand{\isakeywordcharunderscore}{\mbox{-}}%
1.125 +\renewcommand{\isacharbang}{\isamath{!}}%
1.126 +\renewcommand{\isachardoublequote}{}%
1.127 +\renewcommand{\isacharhash}{\isamath{\#}}%
1.128 +\renewcommand{\isachardollar}{\isamath{\$}}%
1.129 +\renewcommand{\isacharpercent}{\isamath{\%}}%
1.130 +\renewcommand{\isacharampersand}{\isamath{\&}}%
1.131 +\renewcommand{\isacharprime}{\isamath{\mskip2mu{'}\mskip-2mu}}%
1.132 +\renewcommand{\isacharparenleft}{\isamath{(}}%
1.133 +\renewcommand{\isacharparenright}{\isamath{)}}%
1.134 +\renewcommand{\isacharasterisk}{\isamath{*}}%
1.135 +\renewcommand{\isacharplus}{\isamath{+}}%
1.136 +\renewcommand{\isacharcomma}{\isamath{\mathord,}}%
1.137 +\renewcommand{\isacharminus}{\isamath{-}}%
1.138 +\renewcommand{\isachardot}{\isamath{\mathord.}}%
1.139 +\renewcommand{\isacharslash}{\isamath{/}}%
1.140 +\renewcommand{\isacharcolon}{\isamath{\mathord:}}%
1.141 +\renewcommand{\isacharsemicolon}{\isamath{\mathord;}}%
1.142 +\renewcommand{\isacharless}{\isamath{<}}%
1.143 +\renewcommand{\isacharequal}{\isamath{=}}%
1.144 +\renewcommand{\isachargreater}{\isamath{>}}%
1.145 +\renewcommand{\isacharat}{\isamath{@}}%
1.146 +\renewcommand{\isacharbrackleft}{\isamath{[}}%
1.147 +\renewcommand{\isacharbrackright}{\isamath{]}}%
1.148 +\renewcommand{\isacharunderscore}{\mbox{-}}%
1.149 +\renewcommand{\isacharbraceleft}{\isamath{\{}}%
1.150 +\renewcommand{\isacharbar}{\isamath{\mid}}%
1.151 +\renewcommand{\isacharbraceright}{\isamath{\}}}%
1.152 +\renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}%
1.153 +}
1.154 +
1.155 +\newcommand{\isabellestylesl}{%
1.156 +\isabellestyleit%
1.157 +\renewcommand{\isastyle}{\small\sl}%
1.158 +\renewcommand{\isastyleminor}{\sl}%
1.159 +\renewcommand{\isastylescript}{\footnotesize\sl}%
1.160 +}