2 %% macros for Isabelle generated LaTeX output
5 %%% Simple document preparation (based on theory token language and symbols)
7 % isabelle environments
9 \newcommand{\isabellecontext}{UNKNOWN}
11 \newcommand{\isastyle}{\UNDEF}
12 \newcommand{\isastyleminor}{\UNDEF}
13 \newcommand{\isastylescript}{\UNDEF}
14 \newcommand{\isastyletext}{\normalsize\rm}
15 \newcommand{\isastyletxt}{\rm}
16 \newcommand{\isastylecmt}{\rm}
18 %symbol markup -- \emph achieves decent spacing via italic corrections
19 \newcommand{\isamath}[1]{\emph{$#1$}}
20 \newcommand{\isatext}[1]{\emph{#1}}
21 \DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
22 \newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
23 \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
24 \newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
25 \newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
26 \DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isastylescript}
27 \DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup}
28 \DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isastylescript}
29 \DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}
30 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
31 \newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}}
33 \newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
34 \newcommand{\isaantiqopen}{\isakeyword{\isacharbraceleft}}
35 \newcommand{\isaantiqclose}{\isakeyword{\isacharbraceright}}
37 \newdimen\isa@parindent\newdimen\isa@parskip
39 \newenvironment{isabellebody}{%
41 \isa@parindent\parindent\parindent0pt%
42 \isa@parskip\parskip\parskip0pt%
45 \newenvironment{isabelle}
46 {\begin{trivlist}\begin{isabellebody}\item\relax}
47 {\end{isabellebody}\end{trivlist}}
49 \newcommand{\isa}[1]{\emph{\isastyleminor #1}}
51 \newcommand{\isaindent}[1]{\hphantom{#1}}
52 \newcommand{\isanewline}{\mbox{}\par\mbox{}}
53 \newcommand{\isasep}{}
54 \newcommand{\isadigit}[1]{#1}
56 \newcommand{\isachardefaults}{%
57 \chardef\isacharbang=`\!%
58 \chardef\isachardoublequote=`\"%
59 \chardef\isachardoublequoteopen=`\"%
60 \chardef\isachardoublequoteclose=`\"%
61 \chardef\isacharhash=`\#%
62 \chardef\isachardollar=`\$%
63 \chardef\isacharpercent=`\%%
64 \chardef\isacharampersand=`\&%
65 \chardef\isacharprime=`\'%
66 \chardef\isacharparenleft=`\(%
67 \chardef\isacharparenright=`\)%
68 \chardef\isacharasterisk=`\*%
69 \chardef\isacharplus=`\+%
70 \chardef\isacharcomma=`\,%
71 \chardef\isacharminus=`\-%
72 \chardef\isachardot=`\.%
73 \chardef\isacharslash=`\/%
74 \chardef\isacharcolon=`\:%
75 \chardef\isacharsemicolon=`\;%
76 \chardef\isacharless=`\<%
77 \chardef\isacharequal=`\=%
78 \chardef\isachargreater=`\>%
79 \chardef\isacharquery=`\?%
80 \chardef\isacharat=`\@%
81 \chardef\isacharbrackleft=`\[%
82 \chardef\isacharbackslash=`\\%
83 \chardef\isacharbrackright=`\]%
84 \chardef\isacharcircum=`\^%
85 \chardef\isacharunderscore=`\_%
86 \def\isacharunderscorekeyword{\_}%
87 \chardef\isacharbackquote=`\`%
88 \chardef\isacharbackquoteopen=`\`%
89 \chardef\isacharbackquoteclose=`\`%
90 \chardef\isacharbraceleft=`\{%
91 \chardef\isacharbar=`\|%
92 \chardef\isacharbraceright=`\}%
93 \chardef\isachartilde=`\~%
94 \def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}%
95 \def\isacharverbatimclose{\isacharasterisk\isacharbraceright}%
98 \newcommand{\isaliteral}[2]{#2}
99 \newcommand{\isanil}{}
102 % keyword and section markup
104 \newcommand{\isakeyword}[1]
105 {\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}%
106 \def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
107 \newcommand{\isacommand}[1]{\isakeyword{#1}}
109 \newcommand{\isamarkupheader}[1]{\section{#1}}
110 \newcommand{\isamarkupchapter}[1]{\chapter{#1}}
111 \newcommand{\isamarkupsection}[1]{\section{#1}}
112 \newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
113 \newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
114 \newcommand{\isamarkupsect}[1]{\section{#1}}
115 \newcommand{\isamarkupsubsect}[1]{\subsection{#1}}
116 \newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
119 \newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
120 \newcommand{\isaendpar}{\par\medskip}
121 \newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
122 \newenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}}{\end{isapar}}
123 \newenvironment{isamarkuptxt}{\par\isastyletxt\begin{isapar}}{\end{isapar}}
124 \newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
129 \def\isabellestyle#1{\csname isabellestyle#1\endcsname}
131 \newcommand{\isabellestyledefault}{%
132 \renewcommand{\isastyle}{\small\tt\slshape}%
133 \renewcommand{\isastyleminor}{\small\tt\slshape}%
134 \renewcommand{\isastylescript}{\footnotesize\tt\slshape}%
137 \isabellestyledefault
139 \newcommand{\isabellestylett}{%
140 \renewcommand{\isastyle}{\small\tt}%
141 \renewcommand{\isastyleminor}{\small\tt}%
142 \renewcommand{\isastylescript}{\footnotesize\tt}%
146 \newcommand{\isabellestyleit}{%
147 \renewcommand{\isastyle}{\small\it}%
148 \renewcommand{\isastyleminor}{\it}%
149 \renewcommand{\isastylescript}{\footnotesize\it}%
150 \renewcommand{\isacharunderscorekeyword}{\mbox{-}}%
151 \renewcommand{\isacharbang}{\isamath{!}}%
152 \renewcommand{\isachardoublequote}{\isanil}%
153 \renewcommand{\isachardoublequoteopen}{\isanil}%
154 \renewcommand{\isachardoublequoteclose}{\isanil}%
155 \renewcommand{\isacharhash}{\isamath{\#}}%
156 \renewcommand{\isachardollar}{\isamath{\$}}%
157 \renewcommand{\isacharpercent}{\isamath{\%}}%
158 \renewcommand{\isacharampersand}{\isamath{\&}}%
159 \renewcommand{\isacharprime}{\isamath{\mskip2mu{'}\mskip-2mu}}%
160 \renewcommand{\isacharparenleft}{\isamath{(}}%
161 \renewcommand{\isacharparenright}{\isamath{)}}%
162 \renewcommand{\isacharasterisk}{\isamath{*}}%
163 \renewcommand{\isacharplus}{\isamath{+}}%
164 \renewcommand{\isacharcomma}{\isamath{\mathord,}}%
165 \renewcommand{\isacharminus}{\isamath{-}}%
166 \renewcommand{\isachardot}{\isamath{\mathord.}}%
167 \renewcommand{\isacharslash}{\isamath{/}}%
168 \renewcommand{\isacharcolon}{\isamath{\mathord:}}%
169 \renewcommand{\isacharsemicolon}{\isamath{\mathord;}}%
170 \renewcommand{\isacharless}{\isamath{<}}%
171 \renewcommand{\isacharequal}{\isamath{=}}%
172 \renewcommand{\isachargreater}{\isamath{>}}%
173 \renewcommand{\isacharat}{\isamath{@}}%
174 \renewcommand{\isacharbrackleft}{\isamath{[}}%
175 \renewcommand{\isacharbackslash}{\isamath{\backslash}}%
176 \renewcommand{\isacharbrackright}{\isamath{]}}%
177 \renewcommand{\isacharunderscore}{\mbox{-}}%
178 \renewcommand{\isacharbraceleft}{\isamath{\{}}%
179 \renewcommand{\isacharbar}{\isamath{\mid}}%
180 \renewcommand{\isacharbraceright}{\isamath{\}}}%
181 \renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}%
182 \renewcommand{\isacharbackquoteopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
183 \renewcommand{\isacharbackquoteclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
184 \renewcommand{\isacharverbatimopen}{\isamath{\langle\!\langle}}%
185 \renewcommand{\isacharverbatimclose}{\isamath{\rangle\!\rangle}}%
188 \newcommand{\isabellestylesl}{%
190 \renewcommand{\isastyle}{\small\sl}%
191 \renewcommand{\isastyleminor}{\sl}%
192 \renewcommand{\isastylescript}{\footnotesize\sl}%
198 %plain TeX version of comment package -- much faster!
199 \let\isafmtname\fmtname\def\fmtname{plain}
201 \let\fmtname\isafmtname
203 \newcommand{\isafold}[1]{\emph{$\langle\mathord{\mathit{#1}}\rangle$}}
205 \newcommand{\isakeeptag}[1]%
206 {\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}}
207 \newcommand{\isadroptag}[1]%
208 {\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}}
209 \newcommand{\isafoldtag}[1]%
210 {\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}}
216 \isadroptag{invisible}
218 \IfFileExists{isabelletags.sty}{\usepackage{isabelletags}}{}