doc-src/TutorialI/Misc/Translations.thy

--- a/doc-src/TutorialI/Misc/Translations.thy	Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Misc/Translations.thy	Thu Jul 26 16:43:02 2001 +0200
@@ -4,34 +4,34 @@
 subsection{*Syntax Translations*}
 
 text{*\label{sec:def-translations}
-\indexbold{syntax translations|(}%
-\indexbold{translations@\isacommand {translations} (command)|(}
-Isabelle offers an additional definition-like facility,
+\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, and this is reversed upon printing. For example,
+replaced by its definition.  This effect 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{$IsaEqTrans@\isasymrightleftharpoons}
+text{*\index{$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}
+@{text"\<rightharpoonup>"}\index{$IsaEqTrans1@\isasymrightharpoonup}
+and @{text"\<leftharpoondown>"}\index{$IsaEqTrans2@\isasymleftharpoondown}
 for uni-directional translations, which only affect
-parsing or printing.  We do not want to cover the details of
-translations at this point.  We have mentioned the concept merely because it
-crops up occasionally: a number of HOL's built-in constructs are defined
+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 @{text"\<noteq>"}, since existing theorems
 about @{text"="} still apply.%
-\indexbold{syntax translations|)}%
-\indexbold{translations@\isacommand {translations} (command)|)}
+\index{syntax translations|)}%
+\index{translations@\isacommand {translations} (command)|)}
 *}
 
 (*<*)