--- a/doc-src/TutorialI/Misc/document/Translations.tex Fri Dec 21 17:31:45 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,48 +0,0 @@
-%
-\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: