equal
deleted
inserted
replaced
29 \newcommand{\isactrlbsub}{\emph\bgroup\begin{math}{}\sb\bgroup\mbox\bgroup\isastylescript} |
29 \newcommand{\isactrlbsub}{\emph\bgroup\begin{math}{}\sb\bgroup\mbox\bgroup\isastylescript} |
30 \newcommand{\isactrlesub}{\egroup\egroup\end{math}\egroup} |
30 \newcommand{\isactrlesub}{\egroup\egroup\end{math}\egroup} |
31 \newcommand{\isactrlbsup}{\emph\bgroup\begin{math}{}\sp\bgroup\mbox\bgroup\isastylescript} |
31 \newcommand{\isactrlbsup}{\emph\bgroup\begin{math}{}\sp\bgroup\mbox\bgroup\isastylescript} |
32 \newcommand{\isactrlesup}{\egroup\egroup\end{math}\egroup} |
32 \newcommand{\isactrlesup}{\egroup\egroup\end{math}\egroup} |
33 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}} |
33 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}} |
|
34 \newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}} |
34 |
35 |
35 |
36 |
36 \newdimen\isa@parindent\newdimen\isa@parskip |
37 \newdimen\isa@parindent\newdimen\isa@parskip |
37 |
38 |
38 \newenvironment{isabellebody}{% |
39 \newenvironment{isabellebody}{% |
47 |
48 |
48 \newcommand{\isa}[1]{\emph{\isastyleminor #1}} |
49 \newcommand{\isa}[1]{\emph{\isastyleminor #1}} |
49 |
50 |
50 \newcommand{\isaindent}[1]{\hphantom{#1}} |
51 \newcommand{\isaindent}[1]{\hphantom{#1}} |
51 \newcommand{\isanewline}{\mbox{}\par\mbox{}} |
52 \newcommand{\isanewline}{\mbox{}\par\mbox{}} |
52 \newcommand{\isasep}{} % override with e.g. \renewcommand{\isasep}{\vspace{1ex}} |
53 \newcommand{\isasep}{} |
53 \newcommand{\isadigit}[1]{#1} |
54 \newcommand{\isadigit}[1]{#1} |
54 |
55 |
55 \chardef\isacharbang=`\! |
56 \chardef\isacharbang=`\! |
56 \chardef\isachardoublequote=`\" |
57 \chardef\isachardoublequote=`\" |
|
58 \chardef\isachardoublequoteopen=`\" |
|
59 \chardef\isachardoublequoteclose=`\" |
57 \chardef\isacharhash=`\# |
60 \chardef\isacharhash=`\# |
58 \chardef\isachardollar=`\$ |
61 \chardef\isachardollar=`\$ |
59 \chardef\isacharpercent=`\% |
62 \chardef\isacharpercent=`\% |
60 \chardef\isacharampersand=`\& |
63 \chardef\isacharampersand=`\& |
61 \chardef\isacharprime=`\' |
64 \chardef\isacharprime=`\' |
78 \chardef\isacharbackslash=`\\ |
81 \chardef\isacharbackslash=`\\ |
79 \chardef\isacharbrackright=`\] |
82 \chardef\isacharbrackright=`\] |
80 \chardef\isacharcircum=`\^ |
83 \chardef\isacharcircum=`\^ |
81 \chardef\isacharunderscore=`\_ |
84 \chardef\isacharunderscore=`\_ |
82 \chardef\isacharbackquote=`\` |
85 \chardef\isacharbackquote=`\` |
|
86 \chardef\isacharbackquoteopen=`\` |
|
87 \chardef\isacharbackquoteclose=`\` |
83 \chardef\isacharbraceleft=`\{ |
88 \chardef\isacharbraceleft=`\{ |
84 \chardef\isacharbar=`\| |
89 \chardef\isacharbar=`\| |
85 \chardef\isacharbraceright=`\} |
90 \chardef\isacharbraceright=`\} |
86 \chardef\isachartilde=`\~ |
91 \chardef\isachartilde=`\~ |
87 |
92 |
127 \renewcommand{\isastyleminor}{\it}% |
132 \renewcommand{\isastyleminor}{\it}% |
128 \renewcommand{\isastylescript}{\footnotesize\it}% |
133 \renewcommand{\isastylescript}{\footnotesize\it}% |
129 \renewcommand{\isakeywordcharunderscore}{\mbox{-}}% |
134 \renewcommand{\isakeywordcharunderscore}{\mbox{-}}% |
130 \renewcommand{\isacharbang}{\isamath{!}}% |
135 \renewcommand{\isacharbang}{\isamath{!}}% |
131 \renewcommand{\isachardoublequote}{}% |
136 \renewcommand{\isachardoublequote}{}% |
|
137 \renewcommand{\isachardoublequoteopen}{}% |
|
138 \renewcommand{\isachardoublequoteclose}{}% |
132 \renewcommand{\isacharhash}{\isamath{\#}}% |
139 \renewcommand{\isacharhash}{\isamath{\#}}% |
133 \renewcommand{\isachardollar}{\isamath{\$}}% |
140 \renewcommand{\isachardollar}{\isamath{\$}}% |
134 \renewcommand{\isacharpercent}{\isamath{\%}}% |
141 \renewcommand{\isacharpercent}{\isamath{\%}}% |
135 \renewcommand{\isacharampersand}{\isamath{\&}}% |
142 \renewcommand{\isacharampersand}{\isamath{\&}}% |
136 \renewcommand{\isacharprime}{\isamath{\mskip2mu{'}\mskip-2mu}}% |
143 \renewcommand{\isacharprime}{\isamath{\mskip2mu{'}\mskip-2mu}}% |
154 \renewcommand{\isacharunderscore}{\mbox{-}}% |
161 \renewcommand{\isacharunderscore}{\mbox{-}}% |
155 \renewcommand{\isacharbraceleft}{\isamath{\{}}% |
162 \renewcommand{\isacharbraceleft}{\isamath{\{}}% |
156 \renewcommand{\isacharbar}{\isamath{\mid}}% |
163 \renewcommand{\isacharbar}{\isamath{\mid}}% |
157 \renewcommand{\isacharbraceright}{\isamath{\}}}% |
164 \renewcommand{\isacharbraceright}{\isamath{\}}}% |
158 \renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}% |
165 \renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}% |
|
166 \renewcommand{\isacharbackquoteopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}% |
|
167 \renewcommand{\isacharbackquoteclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}% |
159 } |
168 } |
160 |
169 |
161 \newcommand{\isabellestylesl}{% |
170 \newcommand{\isabellestylesl}{% |
162 \isabellestyleit% |
171 \isabellestyleit% |
163 \renewcommand{\isastyle}{\small\sl}% |
172 \renewcommand{\isastyle}{\small\sl}% |