equal
deleted
inserted
replaced
1 %% |
1 %% |
2 %% Author: Markus Wenzel, TU Muenchen |
2 %% Author: Markus Wenzel, TU Muenchen |
3 %% |
3 %% |
4 %% macros for Isabelle generated LaTeX output |
4 %% macros for Isabelle generated LaTeX output |
5 %% |
5 %% |
|
6 %% |
6 |
7 |
7 %%% Simple document preparation (based on theory token language and symbols) |
8 %%% Simple document preparation (based on theory token language and symbols) |
8 |
9 |
9 % isabelle environments |
10 % isabelle environments |
10 |
11 |
21 \newcommand{\isamath}[1]{\emph{$#1$}} |
22 \newcommand{\isamath}[1]{\emph{$#1$}} |
22 \newcommand{\isatext}[1]{\emph{#1}} |
23 \newcommand{\isatext}[1]{\emph{#1}} |
23 \newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}} |
24 \newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}} |
24 \newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}} |
25 \newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}} |
25 \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#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{\isactrlbsub}{\emph\bgroup\begin{math}{}\sb\bgroup\mbox\bgroup\isastylescript} |
|
30 \newcommand{\isactrlesub}{\egroup\egroup\end{math}\egroup} |
|
31 \newcommand{\isactrlbsup}{\emph\bgroup\begin{math}{}\sp\bgroup\mbox\bgroup\isastylescript} |
|
32 \newcommand{\isactrlesup}{\egroup\egroup\end{math}\egroup} |
26 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}} |
33 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}} |
|
34 |
27 |
35 |
28 \newdimen\isa@parindent\newdimen\isa@parskip |
36 \newdimen\isa@parindent\newdimen\isa@parskip |
29 |
37 |
30 \newenvironment{isabellebody}{% |
38 \newenvironment{isabellebody}{% |
31 \isamarkuptrue\par% |
39 \isamarkuptrue\par% |
39 |
47 |
40 \newcommand{\isa}[1]{\emph{\isastyleminor #1}} |
48 \newcommand{\isa}[1]{\emph{\isastyleminor #1}} |
41 |
49 |
42 \newcommand{\isaindent}[1]{\hphantom{#1}} |
50 \newcommand{\isaindent}[1]{\hphantom{#1}} |
43 \newcommand{\isanewline}{\mbox{}\par\mbox{}} |
51 \newcommand{\isanewline}{\mbox{}\par\mbox{}} |
|
52 \newcommand{\isasep}{} % override with e.g. \renewcommand{\isasep}{\vspace{1ex}} |
44 \newcommand{\isadigit}[1]{#1} |
53 \newcommand{\isadigit}[1]{#1} |
45 |
54 |
46 \chardef\isacharbang=`\! |
55 \chardef\isacharbang=`\! |
47 \chardef\isachardoublequote=`\" |
56 \chardef\isachardoublequote=`\" |
48 \chardef\isacharhash=`\# |
57 \chardef\isacharhash=`\# |