# HG changeset patch
# User paulson
# Date 984671795 -3600
# Node ID febb93798bb800937271a14e35ba62595d49330f
# Parent  33300d16a63a68cce4ea40e69baf8284c524a508
translations: a tweak

diff -r 33300d16a63a -r febb93798bb8 doc-src/TutorialI/Misc/Translations.thy
--- 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
diff -r 33300d16a63a -r febb93798bb8 doc-src/TutorialI/Misc/document/Translations.tex
--- 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: