2 %% Author: Markus Wenzel, TU Muenchen
3 %% License: GPL (GNU GENERAL PUBLIC LICENSE)
5 %% macros for Isabelle generated LaTeX output
8 %%% Simple document preparation (based on theory token language and symbols)
10 % isabelle environments
12 \newcommand{\isabellecontext}{UNKNOWN}
14 \newcommand{\isastyle}{\small\tt\slshape}
15 \newcommand{\isastyleminor}{\small\tt\slshape}
16 \newcommand{\isastylescript}{\footnotesize\tt\slshape}
17 \newcommand{\isastyletext}{\normalsize\rm}
18 \newcommand{\isastyletxt}{\rm}
19 \newcommand{\isastylecmt}{\rm}
21 %symbol markup -- \emph achieves decent spacing via italic corrections
22 \newcommand{\isamath}[1]{\emph{$#1$}}
23 \newcommand{\isatext}[1]{\emph{#1}}
24 \newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
25 \newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
26 \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
27 \newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
28 \newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
29 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
31 \newdimen\isa@parindent\newdimen\isa@parskip
33 \newenvironment{isabellebody}{%
35 \isa@parindent\parindent\parindent0pt%
36 \isa@parskip\parskip\parskip0pt%
39 \newenvironment{isabelle}
40 {\begin{trivlist}\begin{isabellebody}\item\relax}
41 {\end{isabellebody}\end{trivlist}}
43 \newcommand{\isa}[1]{\emph{\isastyleminor #1}}
45 \newcommand{\isaindent}[1]{\hphantom{#1}}
46 \newcommand{\isanewline}{\mbox{}\par\mbox{}}
47 \newcommand{\isadigit}[1]{#1}
49 \chardef\isacharbang=`\!
50 \chardef\isachardoublequote=`\"
51 \chardef\isacharhash=`\#
52 \chardef\isachardollar=`\$
53 \chardef\isacharpercent=`\%
54 \chardef\isacharampersand=`\&
55 \chardef\isacharprime=`\'
56 \chardef\isacharparenleft=`\(
57 \chardef\isacharparenright=`\)
58 \chardef\isacharasterisk=`\*
59 \chardef\isacharplus=`\+
60 \chardef\isacharcomma=`\,
61 \chardef\isacharminus=`\-
62 \chardef\isachardot=`\.
63 \chardef\isacharslash=`\/
64 \chardef\isacharcolon=`\:
65 \chardef\isacharsemicolon=`\;
66 \chardef\isacharless=`\<
67 \chardef\isacharequal=`\=
68 \chardef\isachargreater=`\>
69 \chardef\isacharquery=`\?
70 \chardef\isacharat=`\@
71 \chardef\isacharbrackleft=`\[
72 \chardef\isacharbackslash=`\\
73 \chardef\isacharbrackright=`\]
74 \chardef\isacharcircum=`\^
75 \chardef\isacharunderscore=`\_
76 \chardef\isacharbackquote=`\`
77 \chardef\isacharbraceleft=`\{
78 \chardef\isacharbar=`\|
79 \chardef\isacharbraceright=`\}
80 \chardef\isachartilde=`\~
83 % keyword and section markup
85 \newcommand{\isakeywordcharunderscore}{\_}
86 \newcommand{\isakeyword}[1]
87 {\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isakeywordcharunderscore}%
88 \def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
89 \newcommand{\isacommand}[1]{\isakeyword{#1}}
91 \newcommand{\isamarkupheader}[1]{\section{#1}}
92 \newcommand{\isamarkupchapter}[1]{\chapter{#1}}
93 \newcommand{\isamarkupsection}[1]{\section{#1}}
94 \newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
95 \newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
96 \newcommand{\isamarkupsect}[1]{\section{#1}}
97 \newcommand{\isamarkupsubsect}[1]{\subsection{#1}}
98 \newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
101 \newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
102 \newcommand{\isaendpar}{\par\medskip}
103 \newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
104 \newenvironment{isamarkuptext}{\isastyletext\begin{isapar}}{\end{isapar}}
105 \newenvironment{isamarkuptxt}{\isastyletxt\begin{isapar}}{\end{isapar}}
106 \newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
111 \newcommand{\isabellestyle}{}
112 \def\isabellestyle#1{\csname isabellestyle#1\endcsname}
114 \newcommand{\isabellestylett}{%
115 \renewcommand{\isastyle}{\small\tt}%
116 \renewcommand{\isastyleminor}{\small\tt}%
117 \renewcommand{\isastylescript}{\footnotesize\tt}%
119 \newcommand{\isabellestyleit}{%
120 \renewcommand{\isastyle}{\small\it}%
121 \renewcommand{\isastyleminor}{\it}%
122 \renewcommand{\isastylescript}{\footnotesize\it}%
123 \renewcommand{\isakeywordcharunderscore}{\mbox{-}}%
124 \renewcommand{\isacharbang}{\isamath{!}}%
125 \renewcommand{\isachardoublequote}{}%
126 \renewcommand{\isacharhash}{\isamath{\#}}%
127 \renewcommand{\isachardollar}{\isamath{\$}}%
128 \renewcommand{\isacharpercent}{\isamath{\%}}%
129 \renewcommand{\isacharampersand}{\isamath{\&}}%
130 \renewcommand{\isacharprime}{\isamath{\mskip2mu{'}\mskip-2mu}}%
131 \renewcommand{\isacharparenleft}{\isamath{(}}%
132 \renewcommand{\isacharparenright}{\isamath{)}}%
133 \renewcommand{\isacharasterisk}{\isamath{*}}%
134 \renewcommand{\isacharplus}{\isamath{+}}%
135 \renewcommand{\isacharcomma}{\isamath{\mathord,}}%
136 \renewcommand{\isacharminus}{\isamath{-}}%
137 \renewcommand{\isachardot}{\isamath{\mathord.}}%
138 \renewcommand{\isacharslash}{\isamath{/}}%
139 \renewcommand{\isacharcolon}{\isamath{\mathord:}}%
140 \renewcommand{\isacharsemicolon}{\isamath{\mathord;}}%
141 \renewcommand{\isacharless}{\isamath{<}}%
142 \renewcommand{\isacharequal}{\isamath{=}}%
143 \renewcommand{\isachargreater}{\isamath{>}}%
144 \renewcommand{\isacharat}{\isamath{@}}%
145 \renewcommand{\isacharbrackleft}{\isamath{[}}%
146 \renewcommand{\isacharbrackright}{\isamath{]}}%
147 \renewcommand{\isacharunderscore}{\mbox{-}}%
148 \renewcommand{\isacharbraceleft}{\isamath{\{}}%
149 \renewcommand{\isacharbar}{\isamath{\mid}}%
150 \renewcommand{\isacharbraceright}{\isamath{\}}}%
151 \renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}%
154 \newcommand{\isabellestylesl}{%
156 \renewcommand{\isastyle}{\small\sl}%
157 \renewcommand{\isastyleminor}{\sl}%
158 \renewcommand{\isastylescript}{\footnotesize\sl}%