updated;
authorwenzelm
Thu Jun 06 15:34:52 2002 +0200 (2002-06-06)
changeset 1320690e5852e55e6
parent 13205 050cd555d3a2
child 13207 0d07e49dc9a5
updated;
doc-src/IsarTut/Tutorial/document/Tutorial.tex
doc-src/IsarTut/Tutorial/document/isabelle.sty
doc-src/IsarTut/Tutorial/document/isabellesym.sty
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/IsarTut/Tutorial/document/Tutorial.tex	Thu Jun 06 15:34:52 2002 +0200
     1.3 @@ -0,0 +1,687 @@
     1.4 +%
     1.5 +\begin{isabellebody}%
     1.6 +\def\isabellecontext{Tutorial}%
     1.7 +\isamarkupfalse%
     1.8 +%
     1.9 +\isamarkupchapter{Introduction%
    1.10 +}
    1.11 +\isamarkuptrue%
    1.12 +%
    1.13 +\isamarkupsection{Step-by-step examples%
    1.14 +}
    1.15 +\isamarkuptrue%
    1.16 +%
    1.17 +\isamarkupsubsection{Summing natural numbers%
    1.18 +}
    1.19 +\isamarkuptrue%
    1.20 +\isacommand{theorem}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i\ {\isacharless}\ n\ {\isacharplus}\ {\isadigit{1}}{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n\ {\isacharasterisk}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequote}\ \ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequote}{\isacharquery}P\ n{\isachardoublequote}{\isacharparenright}\isanewline
    1.21 +\isamarkupfalse%
    1.22 +\isacommand{proof}\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline
    1.23 +\ \ \isamarkupfalse%
    1.24 +\isacommand{case}\ {\isadigit{0}}\isanewline
    1.25 +\ \ \isamarkupfalse%
    1.26 +\isacommand{then}\ \isamarkupfalse%
    1.27 +\isacommand{show}\ {\isachardoublequote}{\isacharquery}P\ {\isadigit{0}}{\isachardoublequote}\ \isamarkupfalse%
    1.28 +\isacommand{by}\ simp\isanewline
    1.29 +\isamarkupfalse%
    1.30 +\isacommand{next}\isanewline
    1.31 +\ \ \isamarkupfalse%
    1.32 +\isacommand{case}\ {\isacharparenleft}Suc\ n{\isacharparenright}\isanewline
    1.33 +\ \ \isamarkupfalse%
    1.34 +\isacommand{let}\ {\isachardoublequote}{\isacharquery}S\ n\ {\isacharequal}\ {\isacharunderscore}{\isachardoublequote}\ {\isacharequal}\ {\isachardoublequote}{\isacharquery}P\ n{\isachardoublequote}\isanewline
    1.35 +\ \ \isamarkupfalse%
    1.36 +\isacommand{have}\ {\isachardoublequote}{\isacharquery}S\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharequal}\ {\isacharquery}S\ n\ {\isacharplus}\ {\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse%
    1.37 +\isacommand{by}\ simp\isanewline
    1.38 +\ \ \isamarkupfalse%
    1.39 +\isacommand{also}\ \isamarkupfalse%
    1.40 +\isacommand{have}\ {\isachardoublequote}{\isacharquery}S\ n\ {\isacharequal}\ n\ {\isacharasterisk}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse%
    1.41 +\isacommand{{\isachardot}}\isanewline
    1.42 +\ \ \isamarkupfalse%
    1.43 +\isacommand{also}\ \isamarkupfalse%
    1.44 +\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isacharplus}\ {\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{2}}{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse%
    1.45 +\isacommand{by}\ simp\isanewline
    1.46 +\ \ \isamarkupfalse%
    1.47 +\isacommand{finally}\ \isamarkupfalse%
    1.48 +\isacommand{show}\ {\isachardoublequote}{\isacharquery}P\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse%
    1.49 +\isacommand{by}\ simp\isanewline
    1.50 +\isamarkupfalse%
    1.51 +\isacommand{qed}\isanewline
    1.52 +\isanewline
    1.53 +\isamarkupfalse%
    1.54 +\isacommand{theorem}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i\ {\isacharless}\ n\ {\isacharplus}\ {\isadigit{1}}{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n\ {\isacharasterisk}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
    1.55 +\isamarkupfalse%
    1.56 +\isacommand{proof}\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline
    1.57 +\ \ \isamarkupfalse%
    1.58 +\isacommand{case}\ {\isadigit{0}}\isanewline
    1.59 +\ \ \isamarkupfalse%
    1.60 +\isacommand{then}\ \isamarkupfalse%
    1.61 +\isacommand{show}\ {\isacharquery}case\ \isamarkupfalse%
    1.62 +\isacommand{by}\ simp\isanewline
    1.63 +\isamarkupfalse%
    1.64 +\isacommand{next}\isanewline
    1.65 +\ \ \isamarkupfalse%
    1.66 +\isacommand{case}\ Suc\isanewline
    1.67 +\ \ \isamarkupfalse%
    1.68 +\isacommand{then}\ \isamarkupfalse%
    1.69 +\isacommand{show}\ {\isacharquery}case\ \isamarkupfalse%
    1.70 +\isacommand{by}\ simp\isanewline
    1.71 +\isamarkupfalse%
    1.72 +\isacommand{qed}\isanewline
    1.73 +\isanewline
    1.74 +\isamarkupfalse%
    1.75 +\isacommand{theorem}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i\ {\isacharless}\ n\ {\isacharplus}\ {\isadigit{1}}{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n\ {\isacharasterisk}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
    1.76 +\ \ \isamarkupfalse%
    1.77 +\isacommand{by}\ {\isacharparenleft}induct\ n{\isacharparenright}\ simp{\isacharunderscore}all\isanewline
    1.78 +\ \ \ \ \isanewline
    1.79 +\isamarkupfalse%
    1.80 +\isacommand{theorem}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i\ {\isacharless}\ n\ {\isacharplus}\ {\isadigit{1}}{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n\ {\isacharasterisk}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
    1.81 +\ \ \isamarkupfalse%
    1.82 +\isacommand{apply}\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline
    1.83 +\ \ \ \isamarkupfalse%
    1.84 +\isacommand{apply}\ simp{\isacharunderscore}all\isanewline
    1.85 +\ \ \isamarkupfalse%
    1.86 +\isacommand{done}\isamarkupfalse%
    1.87 +%
    1.88 +\isamarkupchapter{Interaction and debugging%
    1.89 +}
    1.90 +\isamarkuptrue%
    1.91 +%
    1.92 +\isamarkupchapter{Calculational reasoning%
    1.93 +}
    1.94 +\isamarkuptrue%
    1.95 +%
    1.96 +\isamarkupchapter{Proof by cases and induction%
    1.97 +}
    1.98 +\isamarkuptrue%
    1.99 +%
   1.100 +\isamarkupchapter{General natural deduction%
   1.101 +}
   1.102 +\isamarkuptrue%
   1.103 +%
   1.104 +\isamarkupchapter{Example: FIXME%
   1.105 +}
   1.106 +\isamarkuptrue%
   1.107 +%
   1.108 +\isamarkupchapter{FIXME%
   1.109 +}
   1.110 +\isamarkuptrue%
   1.111 +%
   1.112 +\isamarkupsection{Formal document preparation%
   1.113 +}
   1.114 +\isamarkuptrue%
   1.115 +%
   1.116 +\isamarkupsubsection{Example%
   1.117 +}
   1.118 +\isamarkuptrue%
   1.119 +%
   1.120 +\begin{isamarkuptext}%
   1.121 +See this very document itself.%
   1.122 +\end{isamarkuptext}%
   1.123 +\isamarkuptrue%
   1.124 +%
   1.125 +\isamarkupsubsection{Getting started%
   1.126 +}
   1.127 +\isamarkuptrue%
   1.128 +%
   1.129 +\begin{isamarkuptext}%
   1.130 +\verb"isatool mkdir Test && isatool make"%
   1.131 +\end{isamarkuptext}%
   1.132 +\isamarkuptrue%
   1.133 +%
   1.134 +\isamarkupsection{Human-readable proof composition in Isar%
   1.135 +}
   1.136 +\isamarkuptrue%
   1.137 +%
   1.138 +\isamarkupsubsection{Getting started%
   1.139 +}
   1.140 +\isamarkuptrue%
   1.141 +%
   1.142 +\begin{isamarkuptext}%
   1.143 +Claim a trivial goal in order to enter proof mode \isa{{\isasymdots}}%
   1.144 +\end{isamarkuptext}%
   1.145 +\isamarkuptrue%
   1.146 +\isacommand{lemma}\ True\isanewline
   1.147 +\isamarkupfalse%
   1.148 +\isacommand{proof}\isamarkupfalse%
   1.149 +%
   1.150 +\begin{isamarkuptxt}%
   1.151 +After the canonical initial refinement step we are left
   1.152 +    within an \emph{proof body}.%
   1.153 +\end{isamarkuptxt}%
   1.154 +\isamarkuptrue%
   1.155 +%
   1.156 +\begin{isamarkuptxt}%
   1.157 +Here we may augment the present local {proof context} as we
   1.158 +    please.%
   1.159 +\end{isamarkuptxt}%
   1.160 +\ \ \isamarkuptrue%
   1.161 +\isacommand{fix}\ something\isanewline
   1.162 +\ \ \isamarkupfalse%
   1.163 +\isacommand{assume}\ a{\isacharcolon}\ {\isachardoublequote}anything\ something{\isachardoublequote}\isamarkupfalse%
   1.164 +%
   1.165 +\begin{isamarkuptxt}%
   1.166 +Note that the present configuration may be inspected by
   1.167 +  several \emph{diagnostic commands}.%
   1.168 +\end{isamarkuptxt}%
   1.169 +\ \ \isamarkuptrue%
   1.170 +\isacommand{term}\ something\ \ %
   1.171 +\isamarkupcmt{\isa{something{\isasymColon}{\isacharprime}a}%
   1.172 +}
   1.173 +\isanewline
   1.174 +\ \ \isamarkupfalse%
   1.175 +\isacommand{term}\ anything\ \ %
   1.176 +\isamarkupcmt{\isa{anything{\isasymColon}{\isacharprime}a\ {\isasymRightarrow}\ bool}%
   1.177 +}
   1.178 +\isanewline
   1.179 +\ \ \isamarkupfalse%
   1.180 +\isacommand{thm}\ a\ \ %
   1.181 +\isamarkupcmt{\isa{anything\ something}%
   1.182 +}
   1.183 +\isamarkupfalse%
   1.184 +%
   1.185 +\begin{isamarkuptxt}%
   1.186 +We may state local (auxiliary) results as well.%
   1.187 +\end{isamarkuptxt}%
   1.188 +\ \ \isamarkuptrue%
   1.189 +\isacommand{have}\ True\ \isamarkupfalse%
   1.190 +\isacommand{proof}\ \isamarkupfalse%
   1.191 +\isacommand{qed}\isamarkupfalse%
   1.192 +%
   1.193 +\begin{isamarkuptxt}%
   1.194 +We are now satisfied.%
   1.195 +\end{isamarkuptxt}%
   1.196 +\isamarkuptrue%
   1.197 +\isacommand{qed}\isamarkupfalse%
   1.198 +%
   1.199 +\isamarkupsubsection{Calculational Reasoning%
   1.200 +}
   1.201 +\isamarkuptrue%
   1.202 +%
   1.203 +\begin{isamarkuptext}%
   1.204 +Isar is mainly about Natural Deduction, but Calculational Reasoning
   1.205 +  turns out as a simplified instance of that, so we demonstrate it
   1.206 +  first.%
   1.207 +\end{isamarkuptext}%
   1.208 +\isamarkuptrue%
   1.209 +%
   1.210 +\isamarkupsubsubsection{Transitive chains%
   1.211 +}
   1.212 +\isamarkuptrue%
   1.213 +%
   1.214 +\begin{isamarkuptext}%
   1.215 +Technique: establish a chain of local facts, separated by \cmd{also}
   1.216 +  and terminated by \cmd{finally}; another goal has to follow to point
   1.217 +  out the final result.%
   1.218 +\end{isamarkuptext}%
   1.219 +\isamarkuptrue%
   1.220 +\isacommand{lemma}\ {\isachardoublequote}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{4}}{\isachardoublequote}\isanewline
   1.221 +\isamarkupfalse%
   1.222 +\isacommand{proof}\ {\isacharminus}\ \ %
   1.223 +\isamarkupcmt{do nothing yet%
   1.224 +}
   1.225 +\isanewline
   1.226 +\ \ \isamarkupfalse%
   1.227 +\isacommand{have}\ {\isachardoublequote}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}{\isachardoublequote}\ \isamarkupfalse%
   1.228 +\isacommand{sorry}\isanewline
   1.229 +\ \ \isamarkupfalse%
   1.230 +\isacommand{also}\isanewline
   1.231 +\ \ \isamarkupfalse%
   1.232 +\isacommand{have}\ {\isachardoublequote}x{\isadigit{2}}\ {\isacharequal}\ x{\isadigit{3}}{\isachardoublequote}\ \isamarkupfalse%
   1.233 +\isacommand{sorry}\isanewline
   1.234 +\ \ \isamarkupfalse%
   1.235 +\isacommand{also}\isanewline
   1.236 +\ \ \isamarkupfalse%
   1.237 +\isacommand{have}\ {\isachardoublequote}x{\isadigit{3}}\ {\isacharequal}\ x{\isadigit{4}}{\isachardoublequote}\ \isamarkupfalse%
   1.238 +\isacommand{sorry}\isanewline
   1.239 +\ \ \isamarkupfalse%
   1.240 +\isacommand{finally}\isanewline
   1.241 +\ \ \isamarkupfalse%
   1.242 +\isacommand{show}\ {\isachardoublequote}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{4}}{\isachardoublequote}\ \isamarkupfalse%
   1.243 +\isacommand{{\isachardot}}\isanewline
   1.244 +\isamarkupfalse%
   1.245 +\isacommand{qed}\isamarkupfalse%
   1.246 +%
   1.247 +\begin{isamarkuptext}%
   1.248 +This may be written more succinctly, using the special term binds
   1.249 +  ``\isa{{\isasymdots}}'' (for the right-hand side of the last statement) and
   1.250 +  ``\isa{{\isacharquery}thesis}'' (for the original claim at the head of the
   1.251 +  proof).%
   1.252 +\end{isamarkuptext}%
   1.253 +\isamarkuptrue%
   1.254 +\isacommand{lemma}\ {\isachardoublequote}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{4}}{\isachardoublequote}\isanewline
   1.255 +\isamarkupfalse%
   1.256 +\isacommand{proof}\ {\isacharminus}\isanewline
   1.257 +\ \ \isamarkupfalse%
   1.258 +\isacommand{have}\ {\isachardoublequote}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}{\isachardoublequote}\ \isamarkupfalse%
   1.259 +\isacommand{sorry}\isanewline
   1.260 +\ \ \isamarkupfalse%
   1.261 +\isacommand{also}\ \isamarkupfalse%
   1.262 +\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isacharequal}\ x{\isadigit{3}}{\isachardoublequote}\ \isamarkupfalse%
   1.263 +\isacommand{sorry}\isanewline
   1.264 +\ \ \isamarkupfalse%
   1.265 +\isacommand{also}\ \isamarkupfalse%
   1.266 +\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isacharequal}\ x{\isadigit{4}}{\isachardoublequote}\ \isamarkupfalse%
   1.267 +\isacommand{sorry}\isanewline
   1.268 +\ \ \isamarkupfalse%
   1.269 +\isacommand{finally}\ \isamarkupfalse%
   1.270 +\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
   1.271 +\isacommand{{\isachardot}}\isanewline
   1.272 +\isamarkupfalse%
   1.273 +\isacommand{qed}\isamarkupfalse%
   1.274 +%
   1.275 +\begin{isamarkuptext}%
   1.276 +The (implicit) forward-chaining steps involved in \cmd{also} and
   1.277 +  \cmd{finally} are declared in the current context.  The main library
   1.278 +  of Isabelle/HOL already knows about (mixed) transitivities of \isa{{\isacharequal}}, \isa{{\isacharless}}, \isa{{\isasymle}} etc.%
   1.279 +\end{isamarkuptext}%
   1.280 +\isamarkuptrue%
   1.281 +\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}x{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ {\isacharless}\ x{\isadigit{6}}{\isachardoublequote}\isanewline
   1.282 +\ \ %
   1.283 +\isamarkupcmt{restriction to type \isa{nat} ensures that \isa{{\isacharless}} is really transitive%
   1.284 +}
   1.285 +\isanewline
   1.286 +\isamarkupfalse%
   1.287 +\isacommand{proof}\ {\isacharminus}\isanewline
   1.288 +\ \ \isamarkupfalse%
   1.289 +\isacommand{have}\ {\isachardoublequote}x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}{\isachardoublequote}\ \isamarkupfalse%
   1.290 +\isacommand{sorry}\isanewline
   1.291 +\ \ \isamarkupfalse%
   1.292 +\isacommand{also}\ \isamarkupfalse%
   1.293 +\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isasymle}\ x{\isadigit{3}}{\isachardoublequote}\ \isamarkupfalse%
   1.294 +\isacommand{sorry}\isanewline
   1.295 +\ \ \isamarkupfalse%
   1.296 +\isacommand{also}\ \isamarkupfalse%
   1.297 +\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isacharequal}\ x{\isadigit{4}}{\isachardoublequote}\ \isamarkupfalse%
   1.298 +\isacommand{sorry}\isanewline
   1.299 +\ \ \isamarkupfalse%
   1.300 +\isacommand{also}\ \isamarkupfalse%
   1.301 +\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isacharless}\ x{\isadigit{5}}{\isachardoublequote}\ \isamarkupfalse%
   1.302 +\isacommand{sorry}\isanewline
   1.303 +\ \ \isamarkupfalse%
   1.304 +\isacommand{also}\ \isamarkupfalse%
   1.305 +\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isacharequal}\ x{\isadigit{6}}{\isachardoublequote}\ \isamarkupfalse%
   1.306 +\isacommand{sorry}\isanewline
   1.307 +\ \ \isamarkupfalse%
   1.308 +\isacommand{finally}\ \isamarkupfalse%
   1.309 +\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
   1.310 +\isacommand{{\isachardot}}\isanewline
   1.311 +\isamarkupfalse%
   1.312 +\isacommand{qed}\isamarkupfalse%
   1.313 +%
   1.314 +\begin{isamarkuptext}%
   1.315 +We may also calculate on propositions.%
   1.316 +\end{isamarkuptext}%
   1.317 +\isamarkuptrue%
   1.318 +\isacommand{lemma}\ True\isanewline
   1.319 +\isamarkupfalse%
   1.320 +\isacommand{proof}\isanewline
   1.321 +\ \ \isamarkupfalse%
   1.322 +\isacommand{have}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ B\ {\isasymlongrightarrow}\ C{\isachardoublequote}\ \isamarkupfalse%
   1.323 +\isacommand{sorry}\isanewline
   1.324 +\ \ \isamarkupfalse%
   1.325 +\isacommand{also}\ \isamarkupfalse%
   1.326 +\isacommand{have}\ A\ \isamarkupfalse%
   1.327 +\isacommand{sorry}\isanewline
   1.328 +\ \ \isamarkupfalse%
   1.329 +\isacommand{also}\ \isamarkupfalse%
   1.330 +\isacommand{have}\ B\ \isamarkupfalse%
   1.331 +\isacommand{sorry}\isanewline
   1.332 +\ \ \isamarkupfalse%
   1.333 +\isacommand{finally}\ \isamarkupfalse%
   1.334 +\isacommand{have}\ C\ \isamarkupfalse%
   1.335 +\isacommand{{\isachardot}}\isanewline
   1.336 +\isamarkupfalse%
   1.337 +\isacommand{qed}\isamarkupfalse%
   1.338 +%
   1.339 +\begin{isamarkuptext}%
   1.340 +This is getting pretty close to Dijkstra's preferred proof style.%
   1.341 +\end{isamarkuptext}%
   1.342 +\isamarkuptrue%
   1.343 +\isacommand{lemma}\ True\isanewline
   1.344 +\isamarkupfalse%
   1.345 +\isacommand{proof}\isanewline
   1.346 +\ \ \isamarkupfalse%
   1.347 +\isacommand{have}\ {\isacharbrackleft}trans{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymAnd}X\ Y\ Z{\isachardot}\ X\ {\isasymlongrightarrow}\ Y\ {\isasymLongrightarrow}\ Y\ {\isasymlongrightarrow}\ Z\ {\isasymLongrightarrow}\ X\ {\isasymlongrightarrow}\ Z{\isachardoublequote}\ \isamarkupfalse%
   1.348 +\isacommand{by}\ rules\isanewline
   1.349 +\ \ \isamarkupfalse%
   1.350 +\isacommand{have}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ B{\isachardoublequote}\ \isamarkupfalse%
   1.351 +\isacommand{sorry}\isanewline
   1.352 +\ \ \isamarkupfalse%
   1.353 +\isacommand{also}\ \isamarkupfalse%
   1.354 +\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isasymlongrightarrow}\ C{\isachardoublequote}\ \isamarkupfalse%
   1.355 +\isacommand{sorry}\isanewline
   1.356 +\ \ \isamarkupfalse%
   1.357 +\isacommand{also}\ \isamarkupfalse%
   1.358 +\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isasymlongrightarrow}\ D{\isachardoublequote}\ \isamarkupfalse%
   1.359 +\isacommand{sorry}\isanewline
   1.360 +\ \ \isamarkupfalse%
   1.361 +\isacommand{finally}\ \isamarkupfalse%
   1.362 +\isacommand{have}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ D{\isachardoublequote}\ \isamarkupfalse%
   1.363 +\isacommand{{\isachardot}}\isanewline
   1.364 +\isamarkupfalse%
   1.365 +\isacommand{qed}\isamarkupfalse%
   1.366 +%
   1.367 +\isamarkupsubsubsection{Degenerate calculations and bigstep reasoning%
   1.368 +}
   1.369 +\isamarkuptrue%
   1.370 +%
   1.371 +\begin{isamarkuptext}%
   1.372 +Instead of \cmd{also}/\cmd{finally} we may use degenerative steps
   1.373 +  \cmd{moreover}/\cmd{ultimately} to accumulate facts, without
   1.374 +  applying any forward rules yet.%
   1.375 +\end{isamarkuptext}%
   1.376 +\isamarkuptrue%
   1.377 +\isacommand{lemma}\ True\isanewline
   1.378 +\isamarkupfalse%
   1.379 +\isacommand{proof}\isanewline
   1.380 +\ \ \isamarkupfalse%
   1.381 +\isacommand{have}\ A\ \isamarkupfalse%
   1.382 +\isacommand{sorry}\isanewline
   1.383 +\ \ \isamarkupfalse%
   1.384 +\isacommand{moreover}\ \isamarkupfalse%
   1.385 +\isacommand{have}\ B\ \isamarkupfalse%
   1.386 +\isacommand{sorry}\isanewline
   1.387 +\ \ \isamarkupfalse%
   1.388 +\isacommand{moreover}\ \isamarkupfalse%
   1.389 +\isacommand{have}\ C\ \isamarkupfalse%
   1.390 +\isacommand{sorry}\isanewline
   1.391 +\ \ \isamarkupfalse%
   1.392 +\isacommand{ultimately}\ \isamarkupfalse%
   1.393 +\isacommand{have}\ A\ \isakeyword{and}\ B\ \isakeyword{and}\ C\ \isamarkupfalse%
   1.394 +\isacommand{{\isachardot}}\ \ %
   1.395 +\isamarkupcmt{Pretty obvious, right?%
   1.396 +}
   1.397 +\isanewline
   1.398 +\isamarkupfalse%
   1.399 +\isacommand{qed}\isamarkupfalse%
   1.400 +%
   1.401 +\begin{isamarkuptext}%
   1.402 +Both kinds of calculational elements may be used together.%
   1.403 +\end{isamarkuptext}%
   1.404 +\isamarkuptrue%
   1.405 +\isacommand{lemma}\ True\isanewline
   1.406 +\isamarkupfalse%
   1.407 +\isacommand{proof}\isanewline
   1.408 +\ \ \isamarkupfalse%
   1.409 +\isacommand{assume}\ reasoning{\isacharunderscore}pattern\ {\isacharbrackleft}trans{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}A\ {\isasymLongrightarrow}\ B\ {\isasymLongrightarrow}\ C\ {\isasymLongrightarrow}\ D{\isachardoublequote}\isanewline
   1.410 +\ \ \isamarkupfalse%
   1.411 +\isacommand{have}\ A\ \isamarkupfalse%
   1.412 +\isacommand{sorry}\isanewline
   1.413 +\ \ \isamarkupfalse%
   1.414 +\isacommand{moreover}\ \isamarkupfalse%
   1.415 +\isacommand{have}\ B\ \isamarkupfalse%
   1.416 +\isacommand{sorry}\isanewline
   1.417 +\ \ \isamarkupfalse%
   1.418 +\isacommand{moreover}\ \isamarkupfalse%
   1.419 +\isacommand{have}\ C\ \isamarkupfalse%
   1.420 +\isacommand{sorry}\isanewline
   1.421 +\ \ \isamarkupfalse%
   1.422 +\isacommand{finally}\ \isamarkupfalse%
   1.423 +\isacommand{have}\ D\ \isamarkupfalse%
   1.424 +\isacommand{{\isachardot}}\isanewline
   1.425 +\isamarkupfalse%
   1.426 +\isacommand{qed}\isamarkupfalse%
   1.427 +%
   1.428 +\isamarkupsubsection{Natural deduction%
   1.429 +}
   1.430 +\isamarkuptrue%
   1.431 +%
   1.432 +\isamarkupsubsubsection{Primitive patterns%
   1.433 +}
   1.434 +\isamarkuptrue%
   1.435 +%
   1.436 +\begin{isamarkuptext}%
   1.437 +The default theory context admits to perform canonical single-step
   1.438 +  reasoning (similar to Gentzen) without further ado.%
   1.439 +\end{isamarkuptext}%
   1.440 +\isamarkuptrue%
   1.441 +\isacommand{lemma}\ True\isanewline
   1.442 +\isamarkupfalse%
   1.443 +\isacommand{proof}\isanewline
   1.444 +\isanewline
   1.445 +\ \ \isamarkupfalse%
   1.446 +\isacommand{have}\ True\ \isamarkupfalse%
   1.447 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   1.448 +\isanewline
   1.449 +\ \ \isamarkupfalse%
   1.450 +\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
   1.451 +\isacommand{assume}\ False\isanewline
   1.452 +\ \ \ \ \isamarkupfalse%
   1.453 +\isacommand{then}\ \isamarkupfalse%
   1.454 +\isacommand{have}\ C\ \isamarkupfalse%
   1.455 +\isacommand{{\isachardot}{\isachardot}}\ \isamarkupfalse%
   1.456 +\isacommand{{\isacharbraceright}}\isanewline
   1.457 +\isanewline
   1.458 +\ \ \isamarkupfalse%
   1.459 +\isacommand{have}\ {\isachardoublequote}{\isasymnot}\ A{\isachardoublequote}\isanewline
   1.460 +\ \ \isamarkupfalse%
   1.461 +\isacommand{proof}\isanewline
   1.462 +\ \ \ \ \isamarkupfalse%
   1.463 +\isacommand{assume}\ A\isanewline
   1.464 +\ \ \ \ \isamarkupfalse%
   1.465 +\isacommand{show}\ False\ \isamarkupfalse%
   1.466 +\isacommand{sorry}\isanewline
   1.467 +\ \ \isamarkupfalse%
   1.468 +\isacommand{qed}\isanewline
   1.469 +\isanewline
   1.470 +\ \ \isamarkupfalse%
   1.471 +\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
   1.472 +\isacommand{assume}\ {\isachardoublequote}{\isasymnot}\ A{\isachardoublequote}\ \isakeyword{and}\ A\isanewline
   1.473 +\ \ \ \ \isamarkupfalse%
   1.474 +\isacommand{then}\ \isamarkupfalse%
   1.475 +\isacommand{have}\ C\ \isamarkupfalse%
   1.476 +\isacommand{{\isachardot}{\isachardot}}\ \isamarkupfalse%
   1.477 +\isacommand{{\isacharbraceright}}\isanewline
   1.478 +\isanewline
   1.479 +\ \ \isamarkupfalse%
   1.480 +\isacommand{have}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ B{\isachardoublequote}\isanewline
   1.481 +\ \ \isamarkupfalse%
   1.482 +\isacommand{proof}\isanewline
   1.483 +\ \ \ \ \isamarkupfalse%
   1.484 +\isacommand{assume}\ A\isanewline
   1.485 +\ \ \ \ \isamarkupfalse%
   1.486 +\isacommand{show}\ B\ \isamarkupfalse%
   1.487 +\isacommand{sorry}\isanewline
   1.488 +\ \ \isamarkupfalse%
   1.489 +\isacommand{qed}\isanewline
   1.490 +\isanewline
   1.491 +\ \ \isamarkupfalse%
   1.492 +\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
   1.493 +\isacommand{assume}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ B{\isachardoublequote}\ \isakeyword{and}\ A\isanewline
   1.494 +\ \ \ \ \isamarkupfalse%
   1.495 +\isacommand{then}\ \isamarkupfalse%
   1.496 +\isacommand{have}\ B\ \isamarkupfalse%
   1.497 +\isacommand{{\isachardot}{\isachardot}}\ \isamarkupfalse%
   1.498 +\isacommand{{\isacharbraceright}}\isanewline
   1.499 +\isanewline
   1.500 +\ \ \isamarkupfalse%
   1.501 +\isacommand{have}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\isanewline
   1.502 +\ \ \isamarkupfalse%
   1.503 +\isacommand{proof}\isanewline
   1.504 +\ \ \ \ \isamarkupfalse%
   1.505 +\isacommand{show}\ A\ \isamarkupfalse%
   1.506 +\isacommand{sorry}\isanewline
   1.507 +\ \ \ \ \isamarkupfalse%
   1.508 +\isacommand{show}\ B\ \isamarkupfalse%
   1.509 +\isacommand{sorry}\isanewline
   1.510 +\ \ \isamarkupfalse%
   1.511 +\isacommand{qed}\isanewline
   1.512 +\isanewline
   1.513 +\ \ \isamarkupfalse%
   1.514 +\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
   1.515 +\isacommand{assume}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\isanewline
   1.516 +\ \ \ \ \isamarkupfalse%
   1.517 +\isacommand{then}\ \isamarkupfalse%
   1.518 +\isacommand{have}\ A\ \isamarkupfalse%
   1.519 +\isacommand{{\isachardot}{\isachardot}}\ \isamarkupfalse%
   1.520 +\isacommand{{\isacharbraceright}}\isanewline
   1.521 +\isanewline
   1.522 +\ \ \isamarkupfalse%
   1.523 +\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
   1.524 +\isacommand{assume}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\isanewline
   1.525 +\ \ \ \ \isamarkupfalse%
   1.526 +\isacommand{then}\ \isamarkupfalse%
   1.527 +\isacommand{have}\ B\ \isamarkupfalse%
   1.528 +\isacommand{{\isachardot}{\isachardot}}\ \isamarkupfalse%
   1.529 +\isacommand{{\isacharbraceright}}\isanewline
   1.530 +\isanewline
   1.531 +\ \ \isamarkupfalse%
   1.532 +\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
   1.533 +\isacommand{assume}\ A\isanewline
   1.534 +\ \ \ \ \isamarkupfalse%
   1.535 +\isacommand{then}\ \isamarkupfalse%
   1.536 +\isacommand{have}\ {\isachardoublequote}A\ {\isasymor}\ B{\isachardoublequote}\ \isamarkupfalse%
   1.537 +\isacommand{{\isachardot}{\isachardot}}\ \isamarkupfalse%
   1.538 +\isacommand{{\isacharbraceright}}\isanewline
   1.539 +\isanewline
   1.540 +\ \ \isamarkupfalse%
   1.541 +\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
   1.542 +\isacommand{assume}\ B\isanewline
   1.543 +\ \ \ \ \isamarkupfalse%
   1.544 +\isacommand{then}\ \isamarkupfalse%
   1.545 +\isacommand{have}\ {\isachardoublequote}A\ {\isasymor}\ B{\isachardoublequote}\ \isamarkupfalse%
   1.546 +\isacommand{{\isachardot}{\isachardot}}\ \isamarkupfalse%
   1.547 +\isacommand{{\isacharbraceright}}\isanewline
   1.548 +\isanewline
   1.549 +\ \ \isamarkupfalse%
   1.550 +\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
   1.551 +\isacommand{assume}\ {\isachardoublequote}A\ {\isasymor}\ B{\isachardoublequote}\isanewline
   1.552 +\ \ \ \ \isamarkupfalse%
   1.553 +\isacommand{then}\ \isamarkupfalse%
   1.554 +\isacommand{have}\ C\isanewline
   1.555 +\ \ \ \ \isamarkupfalse%
   1.556 +\isacommand{proof}\isanewline
   1.557 +\ \ \ \ \ \ \isamarkupfalse%
   1.558 +\isacommand{assume}\ A\isanewline
   1.559 +\ \ \ \ \ \ \isamarkupfalse%
   1.560 +\isacommand{then}\ \isamarkupfalse%
   1.561 +\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
   1.562 +\isacommand{sorry}\isanewline
   1.563 +\ \ \ \ \isamarkupfalse%
   1.564 +\isacommand{next}\isanewline
   1.565 +\ \ \ \ \ \ \isamarkupfalse%
   1.566 +\isacommand{assume}\ B\isanewline
   1.567 +\ \ \ \ \ \ \isamarkupfalse%
   1.568 +\isacommand{then}\ \isamarkupfalse%
   1.569 +\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
   1.570 +\isacommand{sorry}\isanewline
   1.571 +\ \ \ \ \isamarkupfalse%
   1.572 +\isacommand{qed}\ \isamarkupfalse%
   1.573 +\isacommand{{\isacharbraceright}}\isanewline
   1.574 +\isanewline
   1.575 +\ \ \isamarkupfalse%
   1.576 +\isacommand{have}\ {\isachardoublequote}{\isasymforall}x{\isachardot}\ P\ x{\isachardoublequote}\isanewline
   1.577 +\ \ \isamarkupfalse%
   1.578 +\isacommand{proof}\isanewline
   1.579 +\ \ \ \ \isamarkupfalse%
   1.580 +\isacommand{fix}\ x\isanewline
   1.581 +\ \ \ \ \isamarkupfalse%
   1.582 +\isacommand{show}\ {\isachardoublequote}P\ x{\isachardoublequote}\ \isamarkupfalse%
   1.583 +\isacommand{sorry}\isanewline
   1.584 +\ \ \isamarkupfalse%
   1.585 +\isacommand{qed}\isanewline
   1.586 +\isanewline
   1.587 +\ \ \isamarkupfalse%
   1.588 +\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
   1.589 +\isacommand{assume}\ {\isachardoublequote}{\isasymforall}x{\isachardot}\ P\ x{\isachardoublequote}\isanewline
   1.590 +\ \ \ \ \isamarkupfalse%
   1.591 +\isacommand{then}\ \isamarkupfalse%
   1.592 +\isacommand{have}\ {\isachardoublequote}P\ t{\isachardoublequote}\ \isamarkupfalse%
   1.593 +\isacommand{{\isachardot}{\isachardot}}\ \isamarkupfalse%
   1.594 +\isacommand{{\isacharbraceright}}\isanewline
   1.595 +\isanewline
   1.596 +\ \ \isamarkupfalse%
   1.597 +\isacommand{have}\ {\isachardoublequote}{\isasymexists}x{\isachardot}\ P\ x{\isachardoublequote}\isanewline
   1.598 +\ \ \isamarkupfalse%
   1.599 +\isacommand{proof}\isanewline
   1.600 +\ \ \ \ \isamarkupfalse%
   1.601 +\isacommand{show}\ {\isachardoublequote}P\ t{\isachardoublequote}\ \isamarkupfalse%
   1.602 +\isacommand{sorry}\isanewline
   1.603 +\ \ \isamarkupfalse%
   1.604 +\isacommand{qed}\isanewline
   1.605 +\ \ \isanewline
   1.606 +\ \ \isamarkupfalse%
   1.607 +\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
   1.608 +\isacommand{assume}\ {\isachardoublequote}{\isasymexists}x{\isachardot}\ P\ x{\isachardoublequote}\isanewline
   1.609 +\ \ \ \ \isamarkupfalse%
   1.610 +\isacommand{then}\ \isamarkupfalse%
   1.611 +\isacommand{obtain}\ x\ \isakeyword{where}\ {\isachardoublequote}P\ x{\isachardoublequote}\ \isamarkupfalse%
   1.612 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   1.613 +\ \ \ \ \isamarkupfalse%
   1.614 +\isacommand{note}\ nothing\ \ %
   1.615 +\isamarkupcmt{relax%
   1.616 +}
   1.617 +\ \isamarkupfalse%
   1.618 +\isacommand{{\isacharbraceright}}\isanewline
   1.619 +\isamarkupfalse%
   1.620 +\isacommand{qed}\isamarkupfalse%
   1.621 +%
   1.622 +\begin{isamarkuptext}%
   1.623 +Certainly, this works with derived rules for defined concepts in the
   1.624 +  same manner.  E.g.\ use the simple-typed set-theory of Isabelle/HOL.%
   1.625 +\end{isamarkuptext}%
   1.626 +\isamarkuptrue%
   1.627 +\isacommand{lemma}\ True\isanewline
   1.628 +\isamarkupfalse%
   1.629 +\isacommand{proof}\isanewline
   1.630 +\ \ \isamarkupfalse%
   1.631 +\isacommand{have}\ {\isachardoublequote}y\ {\isasymin}\ {\isacharparenleft}{\isasymInter}x\ {\isasymin}\ A{\isachardot}\ B\ x{\isacharparenright}{\isachardoublequote}\isanewline
   1.632 +\ \ \isamarkupfalse%
   1.633 +\isacommand{proof}\isanewline
   1.634 +\ \ \ \ \isamarkupfalse%
   1.635 +\isacommand{fix}\ x\isanewline
   1.636 +\ \ \ \ \isamarkupfalse%
   1.637 +\isacommand{assume}\ {\isachardoublequote}x\ {\isasymin}\ A{\isachardoublequote}\isanewline
   1.638 +\ \ \ \ \isamarkupfalse%
   1.639 +\isacommand{show}\ {\isachardoublequote}y\ {\isasymin}\ B\ x{\isachardoublequote}\ \isamarkupfalse%
   1.640 +\isacommand{sorry}\isanewline
   1.641 +\ \ \isamarkupfalse%
   1.642 +\isacommand{qed}\isanewline
   1.643 +\isanewline
   1.644 +\ \ \isamarkupfalse%
   1.645 +\isacommand{have}\ {\isachardoublequote}y\ {\isasymin}\ {\isacharparenleft}{\isasymUnion}x\ {\isasymin}\ A{\isachardot}\ B\ x{\isacharparenright}{\isachardoublequote}\isanewline
   1.646 +\ \ \isamarkupfalse%
   1.647 +\isacommand{proof}\isanewline
   1.648 +\ \ \ \ \isamarkupfalse%
   1.649 +\isacommand{show}\ {\isachardoublequote}a\ {\isasymin}\ A{\isachardoublequote}\ \isamarkupfalse%
   1.650 +\isacommand{sorry}\isanewline
   1.651 +\ \ \ \ \isamarkupfalse%
   1.652 +\isacommand{show}\ {\isachardoublequote}y\ {\isasymin}\ B\ a{\isachardoublequote}\ \isamarkupfalse%
   1.653 +\isacommand{sorry}\isanewline
   1.654 +\ \ \isamarkupfalse%
   1.655 +\isacommand{qed}\isanewline
   1.656 +\isamarkupfalse%
   1.657 +\isacommand{qed}\isamarkupfalse%
   1.658 +%
   1.659 +\isamarkupsubsubsection{Variations in structure%
   1.660 +}
   1.661 +\isamarkuptrue%
   1.662 +%
   1.663 +\begin{isamarkuptext}%
   1.664 +The design of the Isar language takes the user seriously%
   1.665 +\end{isamarkuptext}%
   1.666 +\isamarkuptrue%
   1.667 +%
   1.668 +\isamarkupsubsubsection{Generalized elimination%
   1.669 +}
   1.670 +\isamarkuptrue%
   1.671 +%
   1.672 +\isamarkupsubsubsection{Scalable cases and induction%
   1.673 +}
   1.674 +\isamarkuptrue%
   1.675 +%
   1.676 +\isamarkupsection{Assimilating the old tactical style%
   1.677 +}
   1.678 +\isamarkuptrue%
   1.679 +%
   1.680 +\begin{isamarkuptext}%
   1.681 +Improper commands: 
   1.682 +  Observation: every Isar subproof may start with a ``script'' of%
   1.683 +\end{isamarkuptext}%
   1.684 +\isamarkuptrue%
   1.685 +\isamarkupfalse%
   1.686 +\end{isabellebody}%
   1.687 +%%% Local Variables:
   1.688 +%%% mode: latex
   1.689 +%%% TeX-master: "root"
   1.690 +%%% End:
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/doc-src/IsarTut/Tutorial/document/isabelle.sty	Thu Jun 06 15:34:52 2002 +0200
     2.3 @@ -0,0 +1,157 @@
     2.4 +%%
     2.5 +%% Author: Markus Wenzel, TU Muenchen
     2.6 +%% License: GPL (GNU GENERAL PUBLIC LICENSE)
     2.7 +%%
     2.8 +%% macros for Isabelle generated LaTeX output
     2.9 +%%
    2.10 +
    2.11 +%%% Simple document preparation (based on theory token language and symbols)
    2.12 +
    2.13 +% isabelle environments
    2.14 +
    2.15 +\newcommand{\isabellecontext}{UNKNOWN}
    2.16 +
    2.17 +\newcommand{\isastyle}{\small\tt\slshape}
    2.18 +\newcommand{\isastyleminor}{\small\tt\slshape}
    2.19 +\newcommand{\isastylescript}{\footnotesize\tt\slshape}
    2.20 +\newcommand{\isastyletext}{\normalsize\rm}
    2.21 +\newcommand{\isastyletxt}{\rm}
    2.22 +\newcommand{\isastylecmt}{\rm}
    2.23 +
    2.24 +%symbol markup -- \emph achieves decent spacing via italic corrections
    2.25 +\newcommand{\isamath}[1]{\emph{$#1$}}
    2.26 +\newcommand{\isatext}[1]{\emph{#1}}
    2.27 +\newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
    2.28 +\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
    2.29 +\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
    2.30 +\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
    2.31 +
    2.32 +\newdimen\isa@parindent\newdimen\isa@parskip
    2.33 +
    2.34 +\newenvironment{isabellebody}{%
    2.35 +\isamarkuptrue\par%
    2.36 +\isa@parindent\parindent\parindent0pt%
    2.37 +\isa@parskip\parskip\parskip0pt%
    2.38 +\isastyle}{\par}
    2.39 +
    2.40 +\newenvironment{isabelle}
    2.41 +{\begin{trivlist}\begin{isabellebody}\item\relax}
    2.42 +{\end{isabellebody}\end{trivlist}}
    2.43 +
    2.44 +\newcommand{\isa}[1]{\emph{\isastyleminor #1}}
    2.45 +
    2.46 +\newcommand{\isaindent}[1]{\hphantom{#1}}
    2.47 +\newcommand{\isanewline}{\mbox{}\\\mbox{}}
    2.48 +\newcommand{\isadigit}[1]{#1}
    2.49 +
    2.50 +\chardef\isacharbang=`\!
    2.51 +\chardef\isachardoublequote=`\"
    2.52 +\chardef\isacharhash=`\#
    2.53 +\chardef\isachardollar=`\$
    2.54 +\chardef\isacharpercent=`\%
    2.55 +\chardef\isacharampersand=`\&
    2.56 +\chardef\isacharprime=`\'
    2.57 +\chardef\isacharparenleft=`\(
    2.58 +\chardef\isacharparenright=`\)
    2.59 +\chardef\isacharasterisk=`\*
    2.60 +\chardef\isacharplus=`\+
    2.61 +\chardef\isacharcomma=`\,
    2.62 +\chardef\isacharminus=`\-
    2.63 +\chardef\isachardot=`\.
    2.64 +\chardef\isacharslash=`\/
    2.65 +\chardef\isacharcolon=`\:
    2.66 +\chardef\isacharsemicolon=`\;
    2.67 +\chardef\isacharless=`\<
    2.68 +\chardef\isacharequal=`\=
    2.69 +\chardef\isachargreater=`\>
    2.70 +\chardef\isacharquery=`\?
    2.71 +\chardef\isacharat=`\@
    2.72 +\chardef\isacharbrackleft=`\[
    2.73 +\chardef\isacharbackslash=`\\
    2.74 +\chardef\isacharbrackright=`\]
    2.75 +\chardef\isacharcircum=`\^
    2.76 +\chardef\isacharunderscore=`\_
    2.77 +\chardef\isacharbackquote=`\`
    2.78 +\chardef\isacharbraceleft=`\{
    2.79 +\chardef\isacharbar=`\|
    2.80 +\chardef\isacharbraceright=`\}
    2.81 +\chardef\isachartilde=`\~
    2.82 +
    2.83 +
    2.84 +% keyword and section markup
    2.85 +
    2.86 +\newcommand{\isakeywordcharunderscore}{\_}
    2.87 +\newcommand{\isakeyword}[1]
    2.88 +{\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isakeywordcharunderscore}%
    2.89 +\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
    2.90 +\newcommand{\isacommand}[1]{\isakeyword{#1}}
    2.91 +
    2.92 +\newcommand{\isamarkupheader}[1]{\section{#1}}
    2.93 +\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
    2.94 +\newcommand{\isamarkupsection}[1]{\section{#1}}
    2.95 +\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
    2.96 +\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
    2.97 +\newcommand{\isamarkupsect}[1]{\section{#1}}
    2.98 +\newcommand{\isamarkupsubsect}[1]{\subsection{#1}}
    2.99 +\newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
   2.100 +
   2.101 +\newif\ifisamarkup
   2.102 +\newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
   2.103 +\newcommand{\isaendpar}{\par\medskip}
   2.104 +\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
   2.105 +\newenvironment{isamarkuptext}{\isastyletext\begin{isapar}}{\end{isapar}}
   2.106 +\newenvironment{isamarkuptxt}{\isastyletxt\begin{isapar}}{\end{isapar}}
   2.107 +\newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
   2.108 +
   2.109 +
   2.110 +% alternative styles
   2.111 +
   2.112 +\newcommand{\isabellestyle}{}
   2.113 +\def\isabellestyle#1{\csname isabellestyle#1\endcsname}
   2.114 +
   2.115 +\newcommand{\isabellestylett}{%
   2.116 +\renewcommand{\isastyle}{\small\tt}%
   2.117 +\renewcommand{\isastyleminor}{\small\tt}%
   2.118 +\renewcommand{\isastylescript}{\footnotesize\tt}%
   2.119 +}
   2.120 +\newcommand{\isabellestyleit}{%
   2.121 +\renewcommand{\isastyle}{\small\it}%
   2.122 +\renewcommand{\isastyleminor}{\it}%
   2.123 +\renewcommand{\isastylescript}{\footnotesize\it}%
   2.124 +\renewcommand{\isakeywordcharunderscore}{\mbox{-}}%
   2.125 +\renewcommand{\isacharbang}{\isamath{!}}%
   2.126 +\renewcommand{\isachardoublequote}{}%
   2.127 +\renewcommand{\isacharhash}{\isamath{\#}}%
   2.128 +\renewcommand{\isachardollar}{\isamath{\$}}%
   2.129 +\renewcommand{\isacharpercent}{\isamath{\%}}%
   2.130 +\renewcommand{\isacharampersand}{\isamath{\&}}%
   2.131 +\renewcommand{\isacharprime}{\isamath{\mskip2mu{'}\mskip-2mu}}%
   2.132 +\renewcommand{\isacharparenleft}{\isamath{(}}%
   2.133 +\renewcommand{\isacharparenright}{\isamath{)}}%
   2.134 +\renewcommand{\isacharasterisk}{\isamath{*}}%
   2.135 +\renewcommand{\isacharplus}{\isamath{+}}%
   2.136 +\renewcommand{\isacharcomma}{\isamath{\mathord,}}%
   2.137 +\renewcommand{\isacharminus}{\isamath{-}}%
   2.138 +\renewcommand{\isachardot}{\isamath{\mathord.}}%
   2.139 +\renewcommand{\isacharslash}{\isamath{/}}%
   2.140 +\renewcommand{\isacharcolon}{\isamath{\mathord:}}%
   2.141 +\renewcommand{\isacharsemicolon}{\isamath{\mathord;}}%
   2.142 +\renewcommand{\isacharless}{\isamath{<}}%
   2.143 +\renewcommand{\isacharequal}{\isamath{=}}%
   2.144 +\renewcommand{\isachargreater}{\isamath{>}}%
   2.145 +\renewcommand{\isacharat}{\isamath{@}}%
   2.146 +\renewcommand{\isacharbrackleft}{\isamath{[}}%
   2.147 +\renewcommand{\isacharbrackright}{\isamath{]}}%
   2.148 +\renewcommand{\isacharunderscore}{\mbox{-}}%
   2.149 +\renewcommand{\isacharbraceleft}{\isamath{\{}}%
   2.150 +\renewcommand{\isacharbar}{\isamath{\mid}}%
   2.151 +\renewcommand{\isacharbraceright}{\isamath{\}}}%
   2.152 +\renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}%
   2.153 +}
   2.154 +
   2.155 +\newcommand{\isabellestylesl}{%
   2.156 +\isabellestyleit%
   2.157 +\renewcommand{\isastyle}{\small\sl}%
   2.158 +\renewcommand{\isastyleminor}{\sl}%
   2.159 +\renewcommand{\isastylescript}{\footnotesize\sl}%
   2.160 +}
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/doc-src/IsarTut/Tutorial/document/isabellesym.sty	Thu Jun 06 15:34:52 2002 +0200
     3.3 @@ -0,0 +1,354 @@
     3.4 +%%
     3.5 +%% Author: Markus Wenzel, TU Muenchen
     3.6 +%% License: GPL (GNU GENERAL PUBLIC LICENSE)
     3.7 +%%
     3.8 +%% definitions of standard Isabelle symbols
     3.9 +%%
    3.10 +
    3.11 +% symbol definitions
    3.12 +
    3.13 +\newcommand{\isasymzero}{\isatext{\textzerooldstyle}}  %requires textcomp
    3.14 +\newcommand{\isasymone}{\isatext{\textoneoldstyle}}  %requires textcomp
    3.15 +\newcommand{\isasymtwo}{\isatext{\texttwooldstyle}}  %requires textcomp
    3.16 +\newcommand{\isasymthree}{\isatext{\textthreeoldstyle}}  %requires textcomp
    3.17 +\newcommand{\isasymfour}{\isatext{\textfouroldstyle}}  %requires textcomp
    3.18 +\newcommand{\isasymfive}{\isatext{\textfiveoldstyle}}  %requires textcomp
    3.19 +\newcommand{\isasymsix}{\isatext{\textsixoldstyle}}  %requires textcomp
    3.20 +\newcommand{\isasymseven}{\isatext{\textsevenoldstyle}}  %requires textcomp
    3.21 +\newcommand{\isasymeight}{\isatext{\texteightoldstyle}}  %requires textcomp
    3.22 +\newcommand{\isasymnine}{\isatext{\textnineoldstyle}}  %requires textcomp
    3.23 +\newcommand{\isasymA}{\isamath{\mathcal{A}}}
    3.24 +\newcommand{\isasymB}{\isamath{\mathcal{B}}}
    3.25 +\newcommand{\isasymC}{\isamath{\mathcal{C}}}
    3.26 +\newcommand{\isasymD}{\isamath{\mathcal{D}}}
    3.27 +\newcommand{\isasymE}{\isamath{\mathcal{E}}}
    3.28 +\newcommand{\isasymF}{\isamath{\mathcal{F}}}
    3.29 +\newcommand{\isasymG}{\isamath{\mathcal{G}}}
    3.30 +\newcommand{\isasymH}{\isamath{\mathcal{H}}}
    3.31 +\newcommand{\isasymI}{\isamath{\mathcal{I}}}
    3.32 +\newcommand{\isasymJ}{\isamath{\mathcal{J}}}
    3.33 +\newcommand{\isasymK}{\isamath{\mathcal{K}}}
    3.34 +\newcommand{\isasymL}{\isamath{\mathcal{L}}}
    3.35 +\newcommand{\isasymM}{\isamath{\mathcal{M}}}
    3.36 +\newcommand{\isasymN}{\isamath{\mathcal{N}}}
    3.37 +\newcommand{\isasymO}{\isamath{\mathcal{O}}}
    3.38 +\newcommand{\isasymP}{\isamath{\mathcal{P}}}
    3.39 +\newcommand{\isasymQ}{\isamath{\mathcal{Q}}}
    3.40 +\newcommand{\isasymR}{\isamath{\mathcal{R}}}
    3.41 +\newcommand{\isasymS}{\isamath{\mathcal{S}}}
    3.42 +\newcommand{\isasymT}{\isamath{\mathcal{T}}}
    3.43 +\newcommand{\isasymU}{\isamath{\mathcal{U}}}
    3.44 +\newcommand{\isasymV}{\isamath{\mathcal{V}}}
    3.45 +\newcommand{\isasymW}{\isamath{\mathcal{W}}}
    3.46 +\newcommand{\isasymX}{\isamath{\mathcal{X}}}
    3.47 +\newcommand{\isasymY}{\isamath{\mathcal{Y}}}
    3.48 +\newcommand{\isasymZ}{\isamath{\mathcal{Z}}}
    3.49 +\newcommand{\isasyma}{\isamath{\mathrm{a}}}
    3.50 +\newcommand{\isasymb}{\isamath{\mathrm{b}}}
    3.51 +\newcommand{\isasymc}{\isamath{\mathrm{c}}}
    3.52 +\newcommand{\isasymd}{\isamath{\mathrm{d}}}
    3.53 +\newcommand{\isasyme}{\isamath{\mathrm{e}}}
    3.54 +\newcommand{\isasymf}{\isamath{\mathrm{f}}}
    3.55 +\newcommand{\isasymg}{\isamath{\mathrm{g}}}
    3.56 +\newcommand{\isasymh}{\isamath{\mathrm{h}}}
    3.57 +\newcommand{\isasymi}{\isamath{\mathrm{i}}}
    3.58 +\newcommand{\isasymj}{\isamath{\mathrm{j}}}
    3.59 +\newcommand{\isasymk}{\isamath{\mathrm{k}}}
    3.60 +\newcommand{\isasyml}{\isamath{\mathrm{l}}}
    3.61 +\newcommand{\isasymm}{\isamath{\mathrm{m}}}
    3.62 +\newcommand{\isasymn}{\isamath{\mathrm{n}}}
    3.63 +\newcommand{\isasymo}{\isamath{\mathrm{o}}}
    3.64 +\newcommand{\isasymp}{\isamath{\mathrm{p}}}
    3.65 +\newcommand{\isasymq}{\isamath{\mathrm{q}}}
    3.66 +\newcommand{\isasymr}{\isamath{\mathrm{r}}}
    3.67 +\newcommand{\isasyms}{\isamath{\mathrm{s}}}
    3.68 +\newcommand{\isasymt}{\isamath{\mathrm{t}}}
    3.69 +\newcommand{\isasymu}{\isamath{\mathrm{u}}}
    3.70 +\newcommand{\isasymv}{\isamath{\mathrm{v}}}
    3.71 +\newcommand{\isasymw}{\isamath{\mathrm{w}}}
    3.72 +\newcommand{\isasymx}{\isamath{\mathrm{x}}}
    3.73 +\newcommand{\isasymy}{\isamath{\mathrm{y}}}
    3.74 +\newcommand{\isasymz}{\isamath{\mathrm{z}}}
    3.75 +\newcommand{\isasymAA}{\isamath{\mathfrak{A}}}  %requires eufrak
    3.76 +\newcommand{\isasymBB}{\isamath{\mathfrak{B}}}  %requires eufrak
    3.77 +\newcommand{\isasymCC}{\isamath{\mathfrak{C}}}  %requires eufrak
    3.78 +\newcommand{\isasymDD}{\isamath{\mathfrak{D}}}  %requires eufrak
    3.79 +\newcommand{\isasymEE}{\isamath{\mathfrak{E}}}  %requires eufrak
    3.80 +\newcommand{\isasymFF}{\isamath{\mathfrak{F}}}  %requires eufrak
    3.81 +\newcommand{\isasymGG}{\isamath{\mathfrak{G}}}  %requires eufrak
    3.82 +\newcommand{\isasymHH}{\isamath{\mathfrak{H}}}  %requires eufrak
    3.83 +\newcommand{\isasymII}{\isamath{\mathfrak{I}}}  %requires eufrak
    3.84 +\newcommand{\isasymJJ}{\isamath{\mathfrak{J}}}  %requires eufrak
    3.85 +\newcommand{\isasymKK}{\isamath{\mathfrak{K}}}  %requires eufrak
    3.86 +\newcommand{\isasymLL}{\isamath{\mathfrak{L}}}  %requires eufrak
    3.87 +\newcommand{\isasymMM}{\isamath{\mathfrak{M}}}  %requires eufrak
    3.88 +\newcommand{\isasymNN}{\isamath{\mathfrak{N}}}  %requires eufrak
    3.89 +\newcommand{\isasymOO}{\isamath{\mathfrak{O}}}  %requires eufrak
    3.90 +\newcommand{\isasymPP}{\isamath{\mathfrak{P}}}  %requires eufrak
    3.91 +\newcommand{\isasymQQ}{\isamath{\mathfrak{Q}}}  %requires eufrak
    3.92 +\newcommand{\isasymRR}{\isamath{\mathfrak{R}}}  %requires eufrak
    3.93 +\newcommand{\isasymSS}{\isamath{\mathfrak{S}}}  %requires eufrak
    3.94 +\newcommand{\isasymTT}{\isamath{\mathfrak{T}}}  %requires eufrak
    3.95 +\newcommand{\isasymUU}{\isamath{\mathfrak{U}}}  %requires eufrak
    3.96 +\newcommand{\isasymVV}{\isamath{\mathfrak{V}}}  %requires eufrak
    3.97 +\newcommand{\isasymWW}{\isamath{\mathfrak{W}}}  %requires eufrak
    3.98 +\newcommand{\isasymXX}{\isamath{\mathfrak{X}}}  %requires eufrak
    3.99 +\newcommand{\isasymYY}{\isamath{\mathfrak{Y}}}  %requires eufrak
   3.100 +\newcommand{\isasymZZ}{\isamath{\mathfrak{Z}}}  %requires eufrak
   3.101 +\newcommand{\isasymaa}{\isamath{\mathfrak{a}}}  %requires eufrak
   3.102 +\newcommand{\isasymbb}{\isamath{\mathfrak{b}}}  %requires eufrak
   3.103 +\newcommand{\isasymcc}{\isamath{\mathfrak{c}}}  %requires eufrak
   3.104 +\newcommand{\isasymdd}{\isamath{\mathfrak{d}}}  %requires eufrak
   3.105 +\newcommand{\isasymee}{\isamath{\mathfrak{e}}}  %requires eufrak
   3.106 +\newcommand{\isasymff}{\isamath{\mathfrak{f}}}  %requires eufrak
   3.107 +\newcommand{\isasymgg}{\isamath{\mathfrak{g}}}  %requires eufrak
   3.108 +\newcommand{\isasymhh}{\isamath{\mathfrak{h}}}  %requires eufrak
   3.109 +\newcommand{\isasymii}{\isamath{\mathfrak{i}}}  %requires eufrak
   3.110 +\newcommand{\isasymjj}{\isamath{\mathfrak{j}}}  %requires eufrak
   3.111 +\newcommand{\isasymkk}{\isamath{\mathfrak{k}}}  %requires eufrak
   3.112 +\newcommand{\isasymll}{\isamath{\mathfrak{l}}}  %requires eufrak
   3.113 +\newcommand{\isasymmm}{\isamath{\mathfrak{m}}}  %requires eufrak
   3.114 +\newcommand{\isasymnn}{\isamath{\mathfrak{n}}}  %requires eufrak
   3.115 +\newcommand{\isasymoo}{\isamath{\mathfrak{o}}}  %requires eufrak
   3.116 +\newcommand{\isasympp}{\isamath{\mathfrak{p}}}  %requires eufrak
   3.117 +\newcommand{\isasymqq}{\isamath{\mathfrak{q}}}  %requires eufrak
   3.118 +\newcommand{\isasymrr}{\isamath{\mathfrak{r}}}  %requires eufrak
   3.119 +\newcommand{\isasymss}{\isamath{\mathfrak{s}}}  %requires eufrak
   3.120 +\newcommand{\isasymtt}{\isamath{\mathfrak{t}}}  %requires eufrak
   3.121 +\newcommand{\isasymuu}{\isamath{\mathfrak{u}}}  %requires eufrak
   3.122 +\newcommand{\isasymvv}{\isamath{\mathfrak{v}}}  %requires eufrak
   3.123 +\newcommand{\isasymww}{\isamath{\mathfrak{w}}}  %requires eufrak
   3.124 +\newcommand{\isasymxx}{\isamath{\mathfrak{x}}}  %requires eufrak
   3.125 +\newcommand{\isasymyy}{\isamath{\mathfrak{y}}}  %requires eufrak
   3.126 +\newcommand{\isasymzz}{\isamath{\mathfrak{z}}}  %requires eufrak
   3.127 +\newcommand{\isasymalpha}{\isamath{\alpha}}
   3.128 +\newcommand{\isasymbeta}{\isamath{\beta}}
   3.129 +\newcommand{\isasymgamma}{\isamath{\gamma}}
   3.130 +\newcommand{\isasymdelta}{\isamath{\delta}}
   3.131 +\newcommand{\isasymepsilon}{\isamath{\varepsilon}}
   3.132 +\newcommand{\isasymzeta}{\isamath{\zeta}}
   3.133 +\newcommand{\isasymeta}{\isamath{\eta}}
   3.134 +\newcommand{\isasymtheta}{\isamath{\vartheta}}
   3.135 +\newcommand{\isasymiota}{\isamath{\iota}}
   3.136 +\newcommand{\isasymkappa}{\isamath{\kappa}}
   3.137 +\newcommand{\isasymlambda}{\isamath{\lambda}}
   3.138 +\newcommand{\isasymmu}{\isamath{\mu}}
   3.139 +\newcommand{\isasymnu}{\isamath{\nu}}
   3.140 +\newcommand{\isasymxi}{\isamath{\xi}}
   3.141 +\newcommand{\isasympi}{\isamath{\pi}}
   3.142 +\newcommand{\isasymrho}{\isamath{\varrho}}
   3.143 +\newcommand{\isasymsigma}{\isamath{\sigma}}
   3.144 +\newcommand{\isasymtau}{\isamath{\tau}}
   3.145 +\newcommand{\isasymupsilon}{\isamath{\upsilon}}
   3.146 +\newcommand{\isasymphi}{\isamath{\varphi}}
   3.147 +\newcommand{\isasymchi}{\isamath{\chi}}
   3.148 +\newcommand{\isasympsi}{\isamath{\psi}}
   3.149 +\newcommand{\isasymomega}{\isamath{\omega}}
   3.150 +\newcommand{\isasymGamma}{\isamath{\Gamma}}
   3.151 +\newcommand{\isasymDelta}{\isamath{\Delta}}
   3.152 +\newcommand{\isasymTheta}{\isamath{\Theta}}
   3.153 +\newcommand{\isasymLambda}{\isamath{\Lambda}}
   3.154 +\newcommand{\isasymXi}{\isamath{\Xi}}
   3.155 +\newcommand{\isasymPi}{\isamath{\Pi}}
   3.156 +\newcommand{\isasymSigma}{\isamath{\Sigma}}
   3.157 +\newcommand{\isasymUpsilon}{\isamath{\Upsilon}}
   3.158 +\newcommand{\isasymPhi}{\isamath{\Phi}}
   3.159 +\newcommand{\isasymPsi}{\isamath{\Psi}}
   3.160 +\newcommand{\isasymOmega}{\isamath{\Omega}}
   3.161 +\newcommand{\isasymbool}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{B}}}
   3.162 +\newcommand{\isasymcomplex}{\isamath{\mathrm{C}\mkern-15mu{\phantom{\mathrm{t}}\vrule}\mkern9mu}}
   3.163 +\newcommand{\isasymnat}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{N}}}
   3.164 +\newcommand{\isasymrat}{\isamath{\mathrm{Q}\mkern-16mu{\phantom{\mathrm{t}}\vrule}\mkern10mu}}
   3.165 +\newcommand{\isasymreal}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{R}}}
   3.166 +\newcommand{\isasymint}{\isamath{\mathsf{Z}\mkern-7.5mu\mathsf{Z}}}
   3.167 +\newcommand{\isasymleftarrow}{\isamath{\leftarrow}}
   3.168 +\newcommand{\isasymlongleftarrow}{\isamath{\longleftarrow}}
   3.169 +\newcommand{\isasymrightarrow}{\isamath{\rightarrow}}
   3.170 +\newcommand{\isasymlongrightarrow}{\isamath{\longrightarrow}}
   3.171 +\newcommand{\isasymLeftarrow}{\isamath{\Leftarrow}}
   3.172 +\newcommand{\isasymLongleftarrow}{\isamath{\Longleftarrow}}
   3.173 +\newcommand{\isasymRightarrow}{\isamath{\Rightarrow}}
   3.174 +\newcommand{\isasymLongrightarrow}{\isamath{\Longrightarrow}}
   3.175 +\newcommand{\isasymleftrightarrow}{\isamath{\leftrightarrow}}
   3.176 +\newcommand{\isasymlongleftrightarrow}{\isamath{\longleftrightarrow}}
   3.177 +\newcommand{\isasymLeftrightarrow}{\isamath{\Leftrightarrow}}
   3.178 +\newcommand{\isasymLongleftrightarrow}{\isamath{\Longleftrightarrow}}
   3.179 +\newcommand{\isasymmapsto}{\isamath{\mapsto}}
   3.180 +\newcommand{\isasymlongmapsto}{\isamath{\longmapsto}}
   3.181 +\newcommand{\isasymmidarrow}{\isamath{\relbar}}
   3.182 +\newcommand{\isasymMidarrow}{\isamath{\Relbar}}
   3.183 +\newcommand{\isasymhookleftarrow}{\isamath{\hookleftarrow}}
   3.184 +\newcommand{\isasymhookrightarrow}{\isamath{\hookrightarrow}}
   3.185 +\newcommand{\isasymleftharpoondown}{\isamath{\leftharpoondown}}
   3.186 +\newcommand{\isasymrightharpoondown}{\isamath{\rightharpoondown}}
   3.187 +\newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}}
   3.188 +\newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
   3.189 +\newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
   3.190 +\newcommand{\isasymleadsto}{\isamath{\leadsto}}  %requires latexsym
   3.191 +\newcommand{\isasymup}{\isamath{\uparrow}}
   3.192 +\newcommand{\isasymUp}{\isamath{\Uparrow}}
   3.193 +\newcommand{\isasymdown}{\isamath{\downarrow}}
   3.194 +\newcommand{\isasymDown}{\isamath{\Downarrow}}
   3.195 +\newcommand{\isasymupdown}{\isamath{\updownarrow}}
   3.196 +\newcommand{\isasymUpdown}{\isamath{\Updownarrow}}
   3.197 +\newcommand{\isasymlangle}{\isamath{\langle}}
   3.198 +\newcommand{\isasymrangle}{\isamath{\rangle}}
   3.199 +\newcommand{\isasymlceil}{\isamath{\lceil}}
   3.200 +\newcommand{\isasymrceil}{\isamath{\rceil}}
   3.201 +\newcommand{\isasymlfloor}{\isamath{\lfloor}}
   3.202 +\newcommand{\isasymrfloor}{\isamath{\rfloor}}
   3.203 +\newcommand{\isasymlparr}{\isamath{\mathopen{(\mkern-3mu\mid}}}
   3.204 +\newcommand{\isasymrparr}{\isamath{\mathclose{\mid\mkern-3mu)}}}
   3.205 +\newcommand{\isasymlbrakk}{\isamath{\mathopen{\lbrack\mkern-3mu\lbrack}}}
   3.206 +\newcommand{\isasymrbrakk}{\isamath{\mathclose{\rbrack\mkern-3mu\rbrack}}}
   3.207 +\newcommand{\isasymlbrace}{\isamath{\mathopen{\lbrace\mkern-4.5mu\mid}}}
   3.208 +\newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.5mu\rbrace}}}
   3.209 +\newcommand{\isasymguillemotleft}{\isatext{\flqq}}  %requires babel
   3.210 +\newcommand{\isasymguillemotright}{\isatext{\frqq}}  %requires babel
   3.211 +\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
   3.212 +\newcommand{\isasymnot}{\isamath{\neg}}
   3.213 +\newcommand{\isasymbottom}{\isamath{\bot}}
   3.214 +\newcommand{\isasymtop}{\isamath{\top}}
   3.215 +\newcommand{\isasymand}{\isamath{\wedge}}
   3.216 +\newcommand{\isasymAnd}{\isamath{\bigwedge}}
   3.217 +\newcommand{\isasymor}{\isamath{\vee}}
   3.218 +\newcommand{\isasymOr}{\isamath{\bigvee}}
   3.219 +\newcommand{\isasymforall}{\isamath{\forall\,}}
   3.220 +\newcommand{\isasymexists}{\isamath{\exists\,}}
   3.221 +\newcommand{\isasymbox}{\isamath{\Box}}  %requires latexsym
   3.222 +\newcommand{\isasymdiamond}{\isamath{\Diamond}}  %requires latexsym
   3.223 +\newcommand{\isasymturnstile}{\isamath{\vdash}}
   3.224 +\newcommand{\isasymTurnstile}{\isamath{\models}}
   3.225 +\newcommand{\isasymtturnstile}{\isamath{\vdash\!\!\!\vdash}}
   3.226 +\newcommand{\isasymTTurnstile}{\isamath{\mid\!\models}}
   3.227 +\newcommand{\isasymstileturn}{\isamath{\dashv}}
   3.228 +\newcommand{\isasymsurd}{\isamath{\surd}}
   3.229 +\newcommand{\isasymle}{\isamath{\le}}
   3.230 +\newcommand{\isasymge}{\isamath{\ge}}
   3.231 +\newcommand{\isasymlless}{\isamath{\ll}}
   3.232 +\newcommand{\isasymggreater}{\isamath{\gg}}
   3.233 +\newcommand{\isasymlesssim}{\isamath{\lesssim}}  %requires amssymb
   3.234 +\newcommand{\isasymgreatersim}{\isamath{\gtrsim}}  %requires amssymb
   3.235 +\newcommand{\isasymlessapprox}{\isamath{\lessapprox}}  %requires amssymb
   3.236 +\newcommand{\isasymgreaterapprox}{\isamath{\gtrapprox}}  %requires amssymb
   3.237 +\newcommand{\isasymin}{\isamath{\in}}
   3.238 +\newcommand{\isasymnotin}{\isamath{\notin}}
   3.239 +\newcommand{\isasymsubset}{\isamath{\subset}}
   3.240 +\newcommand{\isasymsupset}{\isamath{\supset}}
   3.241 +\newcommand{\isasymsubseteq}{\isamath{\subseteq}}
   3.242 +\newcommand{\isasymsupseteq}{\isamath{\supseteq}}
   3.243 +\newcommand{\isasymsqsubset}{\isamath{\sqsubset}}
   3.244 +\newcommand{\isasymsqsupset}{\isamath{\sqsupset}}  %requires latexsym
   3.245 +\newcommand{\isasymsqsubseteq}{\isamath{\sqsubseteq}}
   3.246 +\newcommand{\isasymsqsupseteq}{\isamath{\sqsupseteq}}
   3.247 +\newcommand{\isasyminter}{\isamath{\cap}}
   3.248 +\newcommand{\isasymInter}{\isamath{\bigcap\,}}
   3.249 +\newcommand{\isasymunion}{\isamath{\cup}}
   3.250 +\newcommand{\isasymUnion}{\isamath{\bigcup\,}}
   3.251 +\newcommand{\isasymsqunion}{\isamath{\sqcup}}
   3.252 +\newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}}
   3.253 +\newcommand{\isasymsqinter}{\isamath{\sqcap}}
   3.254 +\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}}  %requires stmaryrd
   3.255 +\newcommand{\isasymuplus}{\isamath{\uplus}}
   3.256 +\newcommand{\isasymUplus}{\isamath{\biguplus\,}}
   3.257 +\newcommand{\isasymnoteq}{\isamath{\not=}}
   3.258 +\newcommand{\isasymsim}{\isamath{\sim}}
   3.259 +\newcommand{\isasymdoteq}{\isamath{\doteq}}
   3.260 +\newcommand{\isasymsimeq}{\isamath{\simeq}}
   3.261 +\newcommand{\isasymapprox}{\isamath{\approx}}
   3.262 +\newcommand{\isasymasymp}{\isamath{\asymp}}
   3.263 +\newcommand{\isasymcong}{\isamath{\cong}}
   3.264 +\newcommand{\isasymsmile}{\isamath{\smile}}
   3.265 +\newcommand{\isasymequiv}{\isamath{\equiv}}
   3.266 +\newcommand{\isasymfrown}{\isamath{\frown}}
   3.267 +\newcommand{\isasympropto}{\isamath{\propto}}
   3.268 +\newcommand{\isasymbowtie}{\isamath{\bowtie}}
   3.269 +\newcommand{\isasymprec}{\isamath{\prec}}
   3.270 +\newcommand{\isasymsucc}{\isamath{\succ}}
   3.271 +\newcommand{\isasympreceq}{\isamath{\preceq}}
   3.272 +\newcommand{\isasymsucceq}{\isamath{\succeq}}
   3.273 +\newcommand{\isasymparallel}{\isamath{\parallel}}
   3.274 +\newcommand{\isasymbar}{\isamath{\mid}}
   3.275 +\newcommand{\isasymplusminus}{\isamath{\pm}}
   3.276 +\newcommand{\isasymminusplus}{\isamath{\mp}}
   3.277 +\newcommand{\isasymtimes}{\isamath{\times}}
   3.278 +\newcommand{\isasymdiv}{\isamath{\div}}
   3.279 +\newcommand{\isasymcdot}{\isamath{\cdot}}
   3.280 +\newcommand{\isasymstar}{\isamath{\star}}
   3.281 +\newcommand{\isasymbullet}{\boldmath\isamath{\mathchoice{\displaystyle{\cdot}}{\textstyle{\cdot}}{\scriptstyle{\bullet}}{\scriptscriptstyle{\bullet}}}}
   3.282 +\newcommand{\isasymcirc}{\isamath{\circ}}
   3.283 +\newcommand{\isasymdagger}{\isamath{\dagger}}
   3.284 +\newcommand{\isasymddagger}{\isamath{\ddagger}}
   3.285 +\newcommand{\isasymlhd}{\isamath{\lhd}}
   3.286 +\newcommand{\isasymrhd}{\isamath{\rhd}}
   3.287 +\newcommand{\isasymunlhd}{\isamath{\unlhd}}
   3.288 +\newcommand{\isasymunrhd}{\isamath{\unrhd}}
   3.289 +\newcommand{\isasymtriangleleft}{\isamath{\triangleleft}}
   3.290 +\newcommand{\isasymtriangleright}{\isamath{\triangleright}}
   3.291 +\newcommand{\isasymtriangle}{\isamath{\triangle}}
   3.292 +\newcommand{\isasymtriangleq}{\isamath{\triangleq}}  %requires amssymb
   3.293 +\newcommand{\isasymoplus}{\isamath{\oplus}}
   3.294 +\newcommand{\isasymOplus}{\isamath{\bigoplus\,}}
   3.295 +\newcommand{\isasymotimes}{\isamath{\otimes}}
   3.296 +\newcommand{\isasymOtimes}{\isamath{\bigotimes\,}}
   3.297 +\newcommand{\isasymodot}{\isamath{\odot}}
   3.298 +\newcommand{\isasymOdot}{\isamath{\bigodot\,}}
   3.299 +\newcommand{\isasymominus}{\isamath{\ominus}}
   3.300 +\newcommand{\isasymoslash}{\isamath{\oslash}}
   3.301 +\newcommand{\isasymdots}{\isamath{\dots}}
   3.302 +\newcommand{\isasymcdots}{\isamath{\cdots}}
   3.303 +\newcommand{\isasymSum}{\isamath{\sum\,}}
   3.304 +\newcommand{\isasymProd}{\isamath{\prod\,}}
   3.305 +\newcommand{\isasymCoprod}{\isamath{\coprod\,}}
   3.306 +\newcommand{\isasyminfinity}{\isamath{\infty}}
   3.307 +\newcommand{\isasymintegral}{\isamath{\int\,}}
   3.308 +\newcommand{\isasymointegral}{\isamath{\oint\,}}
   3.309 +\newcommand{\isasymclubsuit}{\isamath{\clubsuit}}
   3.310 +\newcommand{\isasymdiamondsuit}{\isamath{\diamondsuit}}
   3.311 +\newcommand{\isasymheartsuit}{\isamath{\heartsuit}}
   3.312 +\newcommand{\isasymspadesuit}{\isamath{\spadesuit}}
   3.313 +\newcommand{\isasymaleph}{\isamath{\aleph}}
   3.314 +\newcommand{\isasymemptyset}{\isamath{\emptyset}}
   3.315 +\newcommand{\isasymnabla}{\isamath{\nabla}}
   3.316 +\newcommand{\isasympartial}{\isamath{\partial}}
   3.317 +\newcommand{\isasymRe}{\isamath{\Re}}
   3.318 +\newcommand{\isasymIm}{\isamath{\Im}}
   3.319 +\newcommand{\isasymflat}{\isamath{\flat}}
   3.320 +\newcommand{\isasymnatural}{\isamath{\natural}}
   3.321 +\newcommand{\isasymsharp}{\isamath{\sharp}}
   3.322 +\newcommand{\isasymangle}{\isamath{\angle}}
   3.323 +\newcommand{\isasymcopyright}{\isatext{\rm\copyright}}
   3.324 +\newcommand{\isasymregistered}{\isatext{\rm\textregistered}}
   3.325 +\newcommand{\isasymhyphen}{\isatext{\rm-}}
   3.326 +\newcommand{\isasyminverse}{\isamath{{}^{-1}}}
   3.327 +\newcommand{\isasymonesuperior}{\isamath{\mathonesuperior}}  %requires latin1
   3.328 +\newcommand{\isasymonequarter}{\isatext{\rm\textonequarter}}  %requires latin1
   3.329 +\newcommand{\isasymtwosuperior}{\isamath{\mathtwosuperior}}  %requires latin1
   3.330 +\newcommand{\isasymonehalf}{\isatext{\rm\textonehalf}}  %requires latin1
   3.331 +\newcommand{\isasymthreesuperior}{\isamath{\maththreesuperior}}  %requires latin1
   3.332 +\newcommand{\isasymthreequarters}{\isatext{\rm\textthreequarters}}  %requires latin1
   3.333 +\newcommand{\isasymordfeminine}{\isatext{\rm\textordfeminine}}
   3.334 +\newcommand{\isasymordmasculine}{\isatext{\rm\textordmasculine}}
   3.335 +\newcommand{\isasymsection}{\isatext{\rm\S}}
   3.336 +\newcommand{\isasymparagraph}{\isatext{\rm\P}}
   3.337 +\newcommand{\isasymexclamdown}{\isatext{\rm\textexclamdown}}
   3.338 +\newcommand{\isasymquestiondown}{\isatext{\rm\textquestiondown}}
   3.339 +\newcommand{\isasymeuro}{\isatext{\EUR}}  %requires marvosym
   3.340 +\newcommand{\isasympounds}{\isamath{\pounds}}
   3.341 +\newcommand{\isasymyen}{\isatext{\yen}}  %requires amssymb
   3.342 +\newcommand{\isasymcent}{\isatext{\cent}}  %requires wasysym
   3.343 +\newcommand{\isasymcurrency}{\isatext{\currency}}  %requires wasysym
   3.344 +\newcommand{\isasymdegree}{\isatext{\rm\textdegree}}  %requires latin1
   3.345 +\newcommand{\isasymamalg}{\isamath{\amalg}}
   3.346 +\newcommand{\isasymmho}{\isamath{\mho}}  %requires latexsym
   3.347 +\newcommand{\isasymlozenge}{\isamath{\lozenge}}  %requires amssym
   3.348 +\newcommand{\isasymJoin}{\isamath{\Join}}  %requires latexsym
   3.349 +\newcommand{\isasymwp}{\isamath{\wp}}
   3.350 +\newcommand{\isasymwrong}{\isamath{\wr}}
   3.351 +\newcommand{\isasymstruct}{\isamath{\diamond}}
   3.352 +\newcommand{\isasymacute}{\isatext{\'\relax}}
   3.353 +\newcommand{\isasymindex}{\isatext{\i}}
   3.354 +\newcommand{\isasymdieresis}{\isatext{\"\relax}}
   3.355 +\newcommand{\isasymcedilla}{\isatext{\c\relax}}
   3.356 +\newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
   3.357 +\newcommand{\isasymspacespace}{\isamath{~~}}