--- a/doc-src/TutorialI/Misc/Translations.thy Thu Mar 15 15:05:51 2001 +0100
+++ b/doc-src/TutorialI/Misc/Translations.thy Thu Mar 15 16:56:35 2001 +0100
@@ -6,7 +6,7 @@
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
+They resemble macros: 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:
*}
@@ -20,11 +20,15 @@
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
+for uni-directional translations, which only affect
+parsing or 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. *}
+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 @{text"\<noteq>"}, since existing theorems
+about @{text"="} still apply.
+*}
(*<*)
end
--- a/doc-src/TutorialI/Misc/document/Translations.tex Thu Mar 15 15:05:51 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/Translations.tex Thu Mar 15 16:56:35 2001 +0100
@@ -9,7 +9,7 @@
\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
+They resemble macros: 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}%
@@ -22,11 +22,14 @@
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
+for uni-directional translations, which only affect
+parsing or 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.%
+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.%
\end{isamarkuptext}%
\end{isabellebody}%
%%% Local Variables: