4 %% macros for Isabelle generated LaTeX output
7 %%% Simple document preparation (based on theory token language)
9 % basic isabelle environment
11 \newcommand{\isabelledefaultstyle}{\small\tt\slshape}
12 \newcommand{\isabellestyle}{}
14 \newdimen\isa@parindent\newdimen\isa@parskip
15 \newenvironment{isabelle}{%
16 \isa@parindent\parindent\parindent0pt%
17 \isa@parskip\parskip\parskip0pt%
18 \isabelledefaultstyle\isabellestyle}{}
20 \newcommand{\isa}[1]{\emph{\isabelledefaultstyle\isabellestyle #1}}
22 \newcommand{\isanewline}{\mbox{}\\\mbox{}}
24 \chardef\isabraceleft=`\{
25 \chardef\isabraceright=`\}
27 \chardef\isacircum=`\^
28 \chardef\isabackslash=`\\
31 % keyword and section markup
33 \newcommand{\isacommand}[1]{\emph{\bf #1}}
34 \newcommand{\isakeyword}[1]{\emph{\bf #1}}
35 \newcommand{\isabeginblock}{\isakeyword{\{}}
36 \newcommand{\isaendblock}{\isakeyword{\}}}
38 \newcommand{\isamarkupheader}[1]{\section{#1}}
39 \newcommand{\isamarkupchapter}[1]{\chapter{#1}}
40 \newcommand{\isamarkupsection}[1]{\section{#1}}
41 \newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
42 \newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
43 \newcommand{\isamarkupsect}[1]{\section{#1}}
44 \newcommand{\isamarkupsubsect}[1]{\subsection{#1}}
45 \newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
47 \newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\par\medskip}{\par\smallskip}
48 \newenvironment{isamarkuptext}{\normalsize\rm\begin{isapar}}{\end{isapar}}
49 \newenvironment{isamarkuptxt}{\rm\begin{isapar}}{\end{isapar}}
50 \newcommand{\isamarkupcmt}[1]{{\rm--- #1}}