4 %% macros for Isabelle generated LaTeX output
7 %%% Simple document preparation (based on theory token language)
9 % isabelle environments
11 \newcommand{\isastyle}{\small\tt\slshape}
12 \newcommand{\isastyleminor}{\small\tt\slshape}
13 \newcommand{\isastyletext}{\normalsize\rm}
14 \newcommand{\isastyletxt}{\rm}
15 \newcommand{\isastylecmt}{\rm}
17 \newdimen\isa@parindent\newdimen\isa@parskip
19 \newenvironment{isabellebody}{%
20 \isa@parindent\parindent\parindent0pt%
21 \isa@parskip\parskip\parskip0pt%
24 \newenvironment{isabelle}
25 {\begin{isabellebody}\begin{trivlist}\item\relax}
26 {\end{trivlist}\end{isabellebody}}
28 \newcommand{\isa}[1]{\emph{\isastyleminor #1}}
30 \newcommand{\isanewline}{\mbox{}\\\mbox{}}
31 \newcommand{\isadigit}[1]{#1}
33 \chardef\isacharbang=`\!
34 \chardef\isachardoublequote=`\"
35 \chardef\isacharhash=`\#
36 \chardef\isachardollar=`\$
37 \chardef\isacharpercent=`\%
38 \chardef\isacharampersand=`\&
39 \chardef\isacharprime=`\'
40 \chardef\isacharparenleft=`\(
41 \chardef\isacharparenright=`\)
42 \chardef\isacharasterisk=`\*
43 \chardef\isacharplus=`\+
44 \chardef\isacharcomma=`\,
45 \chardef\isacharminus=`\-
46 \chardef\isachardot=`\.
47 \chardef\isacharslash=`\/
48 \chardef\isacharcolon=`\:
49 \chardef\isacharsemicolon=`\;
50 \chardef\isacharless=`\<
51 \chardef\isacharequal=`\=
52 \chardef\isachargreater=`\>
53 \chardef\isacharquery=`\?
54 \chardef\isacharat=`\@
55 \chardef\isacharbrackleft=`\[
56 \chardef\isacharbackslash=`\\
57 \chardef\isacharbrackright=`\]
58 \chardef\isacharcircum=`\^
59 \chardef\isacharunderscore=`\_
60 \chardef\isacharbackquote=`\`
61 \chardef\isacharbraceleft=`\{
62 \chardef\isacharbar=`\|
63 \chardef\isacharbraceright=`\}
64 \chardef\isachartilde=`\~
67 % keyword and section markup
69 \newcommand{\isakeywordcharunderscore}{\_}
70 \newcommand{\isakeyword}[1]
71 {\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isakeywordcharunderscore}%
72 \def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
73 \newcommand{\isacommand}[1]{\isakeyword{#1}}
75 \newcommand{\isamarkupheader}[1]{\section{#1}}
76 \newcommand{\isamarkupchapter}[1]{\chapter{#1}}
77 \newcommand{\isamarkupsection}[1]{\section{#1}}
78 \newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
79 \newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
80 \newcommand{\isamarkupsect}[1]{\section{#1}}
81 \newcommand{\isamarkupsubsect}[1]{\subsection{#1}}
82 \newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
84 \newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\par\medskip}{\par\smallskip}
85 \newenvironment{isamarkuptext}{\isastyletext\begin{isapar}}{\end{isapar}}
86 \newenvironment{isamarkuptxt}{\isastyletxt\begin{isapar}}{\end{isapar}}
87 \newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
90 % alternative styles -- default is "tt"
92 \newcommand{\isabellestyle}{}
93 \def\isabellestyle#1{\csname isabellestyle#1\endcsname}
95 \newcommand{\isabellestyleit}{%
96 \renewcommand{\isastyle}{\small\it}%
97 \renewcommand{\isastyleminor}{\it}%
98 \renewcommand{\isakeywordcharunderscore}{-}%
99 %\renewcommand{\isadigit}[1]{\emph{$##1$}}
100 \renewcommand{\isacharbang}{\emph{$!$}}%
101 \renewcommand{\isachardoublequote}{}%
102 \renewcommand{\isacharhash}{\emph{$\#$}}%
103 \renewcommand{\isachardollar}{\emph{$\$$}}%
104 \renewcommand{\isacharpercent}{\emph{$\%$}}%
105 \renewcommand{\isacharampersand}{\emph{$\&$}}%
106 \renewcommand{\isacharprime}{$\mskip2mu{'}\mskip-2mu$}%
107 \renewcommand{\isacharparenleft}{\emph{$($}}%
108 \renewcommand{\isacharparenright}{\emph{$)$}}%
109 \renewcommand{\isacharasterisk}{\emph{$*$}}%
110 \renewcommand{\isacharplus}{\emph{$+$}}%
111 \renewcommand{\isacharcomma}{\emph{$\mathord,$}}%
112 \renewcommand{\isacharminus}{\emph{$-$}}%
113 \renewcommand{\isachardot}{\emph{$\mathord.$}}%
114 \renewcommand{\isacharslash}{\emph{$/$}}%
115 \renewcommand{\isacharcolon}{\emph{$\mathord:$}}%
116 \renewcommand{\isacharsemicolon}{\emph{$\mathord;$}}%
117 \renewcommand{\isacharless}{\emph{$<$}}%
118 \renewcommand{\isacharequal}{\emph{$=$}}%
119 \renewcommand{\isachargreater}{\emph{$>$}}%
120 %\renewcommand{\isacharquery}{\emph{$\mathord?$}}%
121 \renewcommand{\isacharat}{\emph{$@$}}%
122 \renewcommand{\isacharbrackleft}{\emph{$[$}}%
123 \renewcommand{\isacharbrackright}{\emph{$]$}}%
124 \renewcommand{\isacharunderscore}{-}%
125 \renewcommand{\isacharbraceleft}{\emph{$\{$}}%
126 \renewcommand{\isacharbar}{\emph{$\mid$}}%
127 \renewcommand{\isacharbraceright}{\emph{$\}$}}%
130 \newcommand{\isabellestylesl}{\isabellestyleit\renewcommand{\isastyle}{\small\slshape}}