equal
deleted
inserted
replaced
29 \renewcommand{\isatagquote}{\begin{quote}} |
29 \renewcommand{\isatagquote}{\begin{quote}} |
30 \renewcommand{\endisatagquote}{\end{quote}} |
30 \renewcommand{\endisatagquote}{\end{quote}} |
31 \newcommand{\quotebreak}{\\[1.2ex]} |
31 \newcommand{\quotebreak}{\\[1.2ex]} |
32 |
32 |
33 %% typewriter text |
33 %% typewriter text |
34 \newenvironment{typewriter}{\renewcommand{\isastyletext}{}% |
|
35 \renewcommand{\isadigit}[1]{{##1}}% |
|
36 \parindent0pt% |
|
37 \makeatletter\isa@parindent0pt\makeatother% |
|
38 \isabellestyle{tt}\isastyle% |
|
39 \fontsize{9pt}{9pt}\selectfont}{} |
|
40 |
|
41 \isakeeptag{quotetypewriter} |
|
42 \renewcommand{\isatagquotetypewriter}{\begin{quote}\begin{typewriter}} |
|
43 \renewcommand{\endisatagquotetypewriter}{\end{typewriter}\end{quote}} |
|
44 |
|
45 \isakeeptag{quotett} |
34 \isakeeptag{quotett} |
46 \renewcommand{\isatagquotett}{\begin{quote}\isabellestyle{tt}\isastyle} |
35 \renewcommand{\isatagquotett}{\begin{quote}\isabellestyle{tt}\isastyle} |
47 \renewcommand{\endisatagquotett}{\end{quote}} |
36 \renewcommand{\endisatagquotett}{\end{quote}} |
48 |
37 |
49 %% a trick |
38 %% a trick |
68 \isakeeptag{mlref} |
57 \isakeeptag{mlref} |
69 \renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{\ML}~~}Reference}\begingroup\def\isastyletext{\rm}\small} |
58 \renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{\ML}~~}Reference}\begingroup\def\isastyletext{\rm}\small} |
70 \renewcommand{\endisatagmlref}{\endgroup} |
59 \renewcommand{\endisatagmlref}{\endgroup} |
71 |
60 |
72 \isabellestyle{it} |
61 \isabellestyle{it} |
|
62 \def\isastylett{\footnotesize\normalfont\ttfamily} |
73 |
63 |
74 |
64 |
75 %%% Local Variables: |
65 %%% Local Variables: |
76 %%% mode: latex |
66 %%% mode: latex |
77 %%% TeX-master: "implementation" |
67 %%% TeX-master: "implementation" |