%
\begin{isabellebody}%
\def\isabellecontext{Translations}%
\isamarkupfalse%
%
\isamarkupsubsection{Syntax Translations%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\label{sec:def-translations}
\index{syntax translations|(}%
\index{translations@\isacommand {translations} (command)|(}
Isabelle offers an additional definitional facility,
\textbf{syntax translations}.
They resemble macros: upon parsing, the defined concept is immediately
replaced by its definition. This effect is reversed upon printing. For example,
the symbol \isa{{\isasymnoteq}} is defined via a syntax translation:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{translations}\ {\isachardoublequote}x\ {\isasymnoteq}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isasymnot}{\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
%
\begin{isamarkuptext}%
\index{$IsaEqTrans@\isasymrightleftharpoons}
\noindent
Internally, \isa{{\isasymnoteq}} never appears.
In addition to \isa{{\isasymrightleftharpoons}} there are
\isa{{\isasymrightharpoonup}}\index{$IsaEqTrans1@\isasymrightharpoonup}
and \isa{{\isasymleftharpoondown}}\index{$IsaEqTrans2@\isasymleftharpoondown}
for uni-directional translations, which only affect
parsing or printing. This tutorial will not cover the details of
translations. We have mentioned the concept merely because it
crops up occasionally; a number of HOL's built-in constructs are defined
via translations. Translations are preferable to definitions when the new
concept is a trivial variation on an existing one. For example, we
don't need to derive new theorems about \isa{{\isasymnoteq}}, since existing theorems
about \isa{{\isacharequal}} still apply.%
\index{syntax translations|)}%
\index{translations@\isacommand {translations} (command)|)}%
\end{isamarkuptext}%
\isamarkuptrue%
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: