|
11208
|
1 |
%
|
|
|
2 |
\begin{isabellebody}%
|
|
|
3 |
\def\isabellecontext{Translations}%
|
|
|
4 |
%
|
|
|
5 |
\isamarkupsubsection{Syntax Translations%
|
|
|
6 |
}
|
|
|
7 |
%
|
|
|
8 |
\begin{isamarkuptext}%
|
|
|
9 |
\label{sec:def-translations}
|
|
|
10 |
Isabelle offers an additional definition-like facility,
|
|
|
11 |
\textbf{syntax translations}\indexbold{syntax translation}.
|
|
|
12 |
They resemble makros: upon parsing, the defined concept is immediately
|
|
|
13 |
replaced by its definition, and this is reversed upon printing. For example,
|
|
|
14 |
the symbol \isa{{\isasymnoteq}} is defined via a syntax translation:%
|
|
|
15 |
\end{isamarkuptext}%
|
|
|
16 |
\isacommand{translations}\ {\isachardoublequote}x\ {\isasymnoteq}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isasymnot}{\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}%
|
|
|
17 |
\begin{isamarkuptext}%
|
|
|
18 |
\indexbold{*translations}\indexbold{$IsaEqTrans@\isasymrightleftharpoons}
|
|
|
19 |
\noindent
|
|
|
20 |
Internally, \isa{{\isasymnoteq}} never appears.
|
|
|
21 |
|
|
|
22 |
In addition to \isa{{\isasymrightleftharpoons}} there are
|
|
|
23 |
\isa{{\isasymrightharpoonup}}\indexbold{$IsaEqTrans1@\isasymrightharpoonup}
|
|
|
24 |
and \isa{{\isasymleftharpoondown}}\indexbold{$IsaEqTrans2@\isasymleftharpoondown}
|
|
|
25 |
for uni-directional translations (only upon
|
|
|
26 |
parsing respectively printing). We do not want to cover the details of
|
|
|
27 |
translations at this point. We haved mentioned the concept merely because it
|
|
|
28 |
crops up occasionally since a number of HOL's built-in constructs are defined
|
|
|
29 |
via translations.%
|
|
|
30 |
\end{isamarkuptext}%
|
|
|
31 |
\end{isabellebody}%
|
|
|
32 |
%%% Local Variables:
|
|
|
33 |
%%% mode: latex
|
|
|
34 |
%%% TeX-master: "root"
|
|
|
35 |
%%% End:
|