--- a/doc-src/TutorialI/Misc/document/Translations.tex Sun Oct 21 19:48:19 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/Translations.tex Sun Oct 21 19:49:29 2001 +0200
@@ -1,9 +1,11 @@
%
\begin{isabellebody}%
\def\isabellecontext{Translations}%
+\isamarkupfalse%
%
\isamarkupsubsection{Syntax Translations%
}
+\isamarkuptrue%
%
\begin{isamarkuptext}%
\label{sec:def-translations}
@@ -15,7 +17,9 @@
replaced by its definition. This effect is reversed upon printing. For example,
the symbol \isa{{\isasymnoteq}} is defined via a syntax translation:%
\end{isamarkuptext}%
-\isacommand{translations}\ {\isachardoublequote}x\ {\isasymnoteq}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isasymnot}{\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}%
+\isamarkuptrue%
+\isacommand{translations}\ {\isachardoublequote}x\ {\isasymnoteq}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isasymnot}{\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+%
\begin{isamarkuptext}%
\index{$IsaEqTrans@\isasymrightleftharpoons}
\noindent
@@ -35,6 +39,8 @@
\index{syntax translations|)}%
\index{translations@\isacommand {translations} (command)|)}%
\end{isamarkuptext}%
+\isamarkuptrue%
+\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex