6 |
6 |
7 %%% Simple document preparation (based on theory token language) |
7 %%% Simple document preparation (based on theory token language) |
8 |
8 |
9 % isabelle environments |
9 % isabelle environments |
10 |
10 |
11 \newcommand{\isabellestyle}{\small\tt\slshape} |
11 \newcommand{\isastyle}{\small\tt\slshape} |
|
12 \newcommand{\isastyletext}{\normalsize\rm} |
|
13 \newcommand{\isastyletxt}{\rm} |
|
14 \newcommand{\isastylecmt}{\rm} |
12 |
15 |
13 \newdimen\isa@parindent\newdimen\isa@parskip |
16 \newdimen\isa@parindent\newdimen\isa@parskip |
|
17 |
14 \newenvironment{isabelle}{% |
18 \newenvironment{isabelle}{% |
15 \isa@parindent\parindent\parindent0pt% |
19 \isa@parindent\parindent\parindent0pt% |
16 \isa@parskip\parskip\parskip0pt% |
20 \isa@parskip\parskip\parskip0pt% |
17 \isabellestyle}{} |
21 \isastyle}{} |
18 |
22 |
19 \newcommand{\isa}[1]{\emph{\isabellestyle #1}} |
23 \newcommand{\isa}[1]{\emph{\isastyle #1}} |
20 |
|
21 \newenvironment{isabellequote}% |
|
22 {\begin{quote}\begin{isabelle}\noindent}{\end{isabelle}\end{quote}} |
|
23 |
24 |
24 \newcommand{\isanewline}{\mbox{}\\\mbox{}} |
25 \newcommand{\isanewline}{\mbox{}\\\mbox{}} |
25 |
26 |
26 \chardef\isabraceleft=`\{ |
27 \chardef\isacharhash=`\# |
27 \chardef\isabraceright=`\} |
28 \chardef\isachardollar=`\$ |
28 \chardef\isatilde=`\~ |
29 \chardef\isacharpercent=`\% |
29 \chardef\isacircum=`\^ |
30 \chardef\isacharampersand=`\& |
30 \chardef\isabackslash=`\\ |
31 \chardef\isacharprime=`\' |
|
32 \chardef\isacharparenleft=`\( |
|
33 \chardef\isacharparenright=`\) |
|
34 \chardef\isacharasterisk=`\* |
|
35 \chardef\isacharminus=`\- |
|
36 \chardef\isacharless=`\< |
|
37 \chardef\isachargreater=`\> |
|
38 \chardef\isacharbrackleft=`\[ |
|
39 \chardef\isachardoublequote=`\" |
|
40 \chardef\isacharbackslash=`\\ |
|
41 \chardef\isacharbrackright=`\] |
|
42 \chardef\isacharcircum=`\^ |
|
43 \chardef\isacharunderscore=`\_ |
|
44 \chardef\isacharbraceleft=`\{ |
|
45 \chardef\isacharbar=`\| |
|
46 \chardef\isacharbraceright=`\} |
|
47 \chardef\isachartilde=`\~ |
31 |
48 |
32 |
49 |
33 % keyword and section markup |
50 % keyword and section markup |
34 |
51 |
35 \newcommand{\isacommand}[1]{\emph{\bf #1}} |
52 \newcommand{\isacommand}[1]{\emph{\bf #1}} |
45 \newcommand{\isamarkupsect}[1]{\section{#1}} |
62 \newcommand{\isamarkupsect}[1]{\section{#1}} |
46 \newcommand{\isamarkupsubsect}[1]{\subsection{#1}} |
63 \newcommand{\isamarkupsubsect}[1]{\subsection{#1}} |
47 \newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}} |
64 \newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}} |
48 |
65 |
49 \newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\par\medskip}{\par\smallskip} |
66 \newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\par\medskip}{\par\smallskip} |
50 \newenvironment{isamarkuptext}{\normalsize\rm\begin{isapar}}{\end{isapar}} |
67 \newenvironment{isamarkuptext}{\isastyletext\begin{isapar}}{\end{isapar}} |
51 \newenvironment{isamarkuptxt}{\rm\begin{isapar}}{\end{isapar}} |
68 \newenvironment{isamarkuptxt}{\isastyletxt\begin{isapar}}{\end{isapar}} |
52 \newcommand{\isamarkupcmt}[1]{{\rm--- #1}} |
69 \newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}} |
|
70 |
|
71 |
|
72 % alternative styles -- default is "tt" |
|
73 |
|
74 \newcommand{\isabellestyle}{} |
|
75 \def\isabellestyle#1{\csname isasetup#1\endcsname} |
|
76 |
|
77 \newcommand{\isasetupit}{% |
|
78 \renewcommand{\isastyle}{\small\itshape}% |
|
79 \renewcommand{\isastyletext}{\normalsize\rm}% |
|
80 \renewcommand{\isastyletxt}{\rm}% |
|
81 \renewcommand{\isastylecmt}{\rm}% |
|
82 \renewcommand{\isachardollar}{\textsl{\$}}% |
|
83 \renewcommand{\isacharampersand}{\textsl{\&}}% |
|
84 \renewcommand{\isacharprime}{$'$}% |
|
85 \renewcommand{\isacharparenleft}{\emph{$($}}% |
|
86 \renewcommand{\isacharparenright}{\emph{$)$}}% |
|
87 \renewcommand{\isacharasterisk}{\emph{$*$}}% |
|
88 \renewcommand{\isacharminus}{\emph{$-$}}% |
|
89 \renewcommand{\isacharless}{\emph{$<$}}% |
|
90 \renewcommand{\isachargreater}{\emph{$>$}}% |
|
91 \renewcommand{\isachardoublequote}{}% |
|
92 \renewcommand{\isacharbrackleft}{\emph{$[$}}% |
|
93 \renewcommand{\isacharbrackright}{\emph{$]$}}% |
|
94 \renewcommand{\isacharunderscore}{-}% |
|
95 \renewcommand{\isacharbraceleft}{\emph{$\{$}}% |
|
96 \renewcommand{\isacharbar}{\emph{$\mid$}}% |
|
97 \renewcommand{\isacharbraceright}{\emph{$\}$}}% |
|
98 } |
|
99 |
|
100 \newcommand{\isasetupsl}{\isasetupit\renewcommand{\isastyle}{\small\slshape}} |
|
101 |