# HG changeset patch
# User nipkow
# Date 984650793 -3600
# Node ID 76bc8ea0c6f2f791cbb8f39c83503bccba17c0c3
# Parent  08188224c24e9d34f21de390d49f4a4180947e5c
*** empty log message ***

diff -r 08188224c24e -r 76bc8ea0c6f2 doc-src/TutorialI/Misc/Translations.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Misc/Translations.thy	Thu Mar 15 11:06:33 2001 +0100
@@ -0,0 +1,31 @@
+(*<*)
+theory Translations = Main:
+(*>*)
+subsection{*Syntax Translations*}
+
+text{*\label{sec:def-translations}
+Isabelle offers an additional definition-like facility,
+\textbf{syntax translations}\indexbold{syntax translation}.
+They resemble makros: upon parsing, the defined concept is immediately
+replaced by its definition, and this is reversed upon printing. For example,
+the symbol @{text"\<noteq>"} is defined via a syntax translation:
+*}
+
+translations "x \<noteq> y" \<rightleftharpoons> "\<not>(x = y)"
+
+text{*\indexbold{*translations}\indexbold{$IsaEqTrans@\isasymrightleftharpoons}
+\noindent
+Internally, @{text"\<noteq>"} never appears.
+
+In addition to @{text"\<rightleftharpoons>"} there are
+@{text"\<rightharpoonup>"}\indexbold{$IsaEqTrans1@\isasymrightharpoonup}
+and @{text"\<leftharpoondown>"}\indexbold{$IsaEqTrans2@\isasymleftharpoondown}
+for uni-directional translations (only upon
+parsing respectively printing).  We do not want to cover the details of
+translations at this point.  We haved mentioned the concept merely because it
+crops up occasionally since a number of HOL's built-in constructs are defined
+via translations.  *}
+
+(*<*)
+end
+(*>*)
diff -r 08188224c24e -r 76bc8ea0c6f2 doc-src/TutorialI/Misc/document/Translations.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Misc/document/Translations.tex	Thu Mar 15 11:06:33 2001 +0100
@@ -0,0 +1,35 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Translations}%
+%
+\isamarkupsubsection{Syntax Translations%
+}
+%
+\begin{isamarkuptext}%
+\label{sec:def-translations}
+Isabelle offers an additional definition-like facility,
+\textbf{syntax translations}\indexbold{syntax translation}.
+They resemble makros: upon parsing, the defined concept is immediately
+replaced by its definition, and this 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}%
+\begin{isamarkuptext}%
+\indexbold{*translations}\indexbold{$IsaEqTrans@\isasymrightleftharpoons}
+\noindent
+Internally, \isa{{\isasymnoteq}} never appears.
+
+In addition to \isa{{\isasymrightleftharpoons}} there are
+\isa{{\isasymrightharpoonup}}\indexbold{$IsaEqTrans1@\isasymrightharpoonup}
+and \isa{{\isasymleftharpoondown}}\indexbold{$IsaEqTrans2@\isasymleftharpoondown}
+for uni-directional translations (only upon
+parsing respectively printing).  We do not want to cover the details of
+translations at this point.  We haved mentioned the concept merely because it
+crops up occasionally since a number of HOL's built-in constructs are defined
+via translations.%
+\end{isamarkuptext}%
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End: