equal
deleted
inserted
replaced
4 %% macros for Isabelle generated LaTeX output |
4 %% macros for Isabelle generated LaTeX output |
5 %% |
5 %% |
6 |
6 |
7 %%% Simple document preparation (based on theory token language) |
7 %%% Simple document preparation (based on theory token language) |
8 |
8 |
9 % basic isabelle environment |
9 % isabelle environments |
10 |
10 |
11 \newcommand{\isabelledefaultstyle}{\small\tt\slshape} |
11 \newcommand{\isabelledefaultstyle}{\small\tt\slshape} |
12 \newcommand{\isabellestyle}{} |
12 \newcommand{\isabellestyle}{} |
13 |
13 |
14 \newdimen\isa@parindent\newdimen\isa@parskip |
14 \newdimen\isa@parindent\newdimen\isa@parskip |
16 \isa@parindent\parindent\parindent0pt% |
16 \isa@parindent\parindent\parindent0pt% |
17 \isa@parskip\parskip\parskip0pt% |
17 \isa@parskip\parskip\parskip0pt% |
18 \isabelledefaultstyle\isabellestyle}{} |
18 \isabelledefaultstyle\isabellestyle}{} |
19 |
19 |
20 \newcommand{\isa}[1]{\emph{\isabelledefaultstyle\isabellestyle #1}} |
20 \newcommand{\isa}[1]{\emph{\isabelledefaultstyle\isabellestyle #1}} |
|
21 |
|
22 \newenvironment{isabellequote}% |
|
23 {\begin{quote}\begin{isabelle}\noindent}{\end{isabelle}\end{quote}} |
21 |
24 |
22 \newcommand{\isanewline}{\mbox{}\\\mbox{}} |
25 \newcommand{\isanewline}{\mbox{}\\\mbox{}} |
23 |
26 |
24 \chardef\isabraceleft=`\{ |
27 \chardef\isabraceleft=`\{ |
25 \chardef\isabraceright=`\} |
28 \chardef\isabraceright=`\} |