# HG changeset patch
# User wenzelm
# Date 1345028844 -7200
# Node ID 754b09cd616f2676a81a02aaf5b673671891243f
# Parent  eed6698b2ba0b4c7f4c351ae11f09251f93f0889
tuned;

diff -r eed6698b2ba0 -r 754b09cd616f doc-src/IsarRef/Thy/Inner_Syntax.thy
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Wed Aug 15 12:54:25 2012 +0200
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Wed Aug 15 13:07:24 2012 +0200
@@ -1052,7 +1052,7 @@
   with all names and binding scopes resolved, but most type
   information still missing.  Explicit type constraints might be given by
   the user, or implicit position information by the system --- both
-  needs to be passed-through carefully by syntax transformations.
+  need to be passed-through carefully by syntax transformations.
 
   Pre-terms are further processed by the so-called \emph{check} and
   \emph{unckeck} phases that are intertwined with type-inference (see
@@ -1170,7 +1170,7 @@
   correspondence of a particular grammar production to some known term
   entity is preserved.
 
-  \item Input type constants (constructors) and type classes ---
+  \item Input of type constants (constructors) and type classes ---
   thanks to explicit syntactic distinction independently on the
   context.
 
@@ -1181,9 +1181,10 @@
   \end{itemize}
 
   In other words, syntax transformations that operate on input terms
-  written as prefix applications are difficult to achieve.  Luckily,
-  this case rarely occurs in practice, because syntax forms to be
-  translated usually correspond to some bits of concrete notation. *}
+  written as prefix applications are difficult to make robust.
+  Luckily, this case rarely occurs in practice, because syntax forms
+  to be translated usually correspond to some bits of concrete
+  notation. *}
 
 
 subsection {* Raw syntax and translations \label{sec:syn-trans} *}
@@ -1271,7 +1272,7 @@
   check wrt.\ existing declarations.  It is conventional to use plain
   identifiers prefixed by a single underscore (e.g.\ @{text
   "_foobar"}).  Names should be chosen with care, to avoid clashes
-  with unrelated syntax declarations.
+  with other syntax declarations.
 
   \medskip The special case of copy production is specified by @{text
   "c = "}@{verbatim "\"\""} (empty string).  It means that the
@@ -1284,7 +1285,7 @@
 
   \item @{command "translations"}~@{text rules} specifies syntactic
   translation rules (i.e.\ macros) as first-order rewrite rules on
-  ASTs (see also \secref{sec:ast}).  The theory context maintains two
+  ASTs (\secref{sec:ast}).  The theory context maintains two
   independent lists translation rules: parse rules (@{verbatim "=>"}
   or @{text "\<rightharpoonup>"}) and print rules (@{verbatim "<="} or @{text "\<leftharpoondown>"}).
   For convenience, both can be specified simultaneously as parse~/
@@ -1412,7 +1413,7 @@
   chosen in order of appearance in the theory definitions.
 
   The configuration options @{attribute syntax_ast_trace} and
-  @{attribute syntax_ast_stats} might help understand this process
+  @{attribute syntax_ast_stats} might help to understand this process
   and diagnose problems.
 
   \begin{warn}
@@ -1484,12 +1485,11 @@
   \end{tabular}}
   \medskip
 
-  The argument list consist of @{text "(c, tr)"} pairs, where @{text
-  "c"} is the syntax name of the syntax constant, term constant or
-  type constructor involved, and @{text "tr"} a function that
-  translates a syntax form @{text "c args"} into @{text "tr args"}.
-  For print translations, the naming convention for such functions is
-  @{text "tr'"} instead of @{text "tr"}.
+  The argument list consists of @{text "(c, tr)"} pairs, where @{text
+  "c"} is the syntax name of the formal entity involved, and @{text
+  "tr"} a function that translates a syntax form @{text "c args"} into
+  @{text "tr args"}.  The ML naming convention for parse translations
+  is @{text "c_tr"} and for print translations @{text "c_tr'"}.
 
   The @{command_ref print_syntax} command displays the sets of names
   associated with the translation functions of a theory under @{text
@@ -1521,7 +1521,7 @@
 
 subsubsection {* The translation strategy *}
 
-text {* The different kinds of translation functions are called during
+text {* The different kinds of translation functions are invoked during
   the transformations between parse trees, ASTs and syntactic terms
   (cf.\ \figref{fig:parse-print}).  Whenever a combination of the form
   @{text "c x\<^sub>1 \<dots> x\<^sub>n"} is encountered, and a translation function
@@ -1536,7 +1536,8 @@
   $ x\<^sub>1 $ \<dots> $ x\<^sub>n"}.  Terms allow more sophisticated transformations
   than ASTs do, typically involving abstractions and bound
   variables. \emph{Typed} print translations may even peek at the type
-  @{text "\<tau>"} of the constant they are invoked on.
+  @{text "\<tau>"} of the constant they are invoked on, although that information
+  may be inaccurate.
 
   Regardless of whether they act on ASTs or terms, translation
   functions called during the parsing process differ from those for
diff -r eed6698b2ba0 -r 754b09cd616f doc-src/IsarRef/Thy/document/Inner_Syntax.tex
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Wed Aug 15 12:54:25 2012 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Wed Aug 15 13:07:24 2012 +0200
@@ -1235,7 +1235,7 @@
   with all names and binding scopes resolved, but most type
   information still missing.  Explicit type constraints might be given by
   the user, or implicit position information by the system --- both
-  needs to be passed-through carefully by syntax transformations.
+  need to be passed-through carefully by syntax transformations.
 
   Pre-terms are further processed by the so-called \emph{check} and
   \emph{unckeck} phases that are intertwined with type-inference (see
@@ -1363,7 +1363,7 @@
   correspondence of a particular grammar production to some known term
   entity is preserved.
 
-  \item Input type constants (constructors) and type classes ---
+  \item Input of type constants (constructors) and type classes ---
   thanks to explicit syntactic distinction independently on the
   context.
 
@@ -1374,9 +1374,10 @@
   \end{itemize}
 
   In other words, syntax transformations that operate on input terms
-  written as prefix applications are difficult to achieve.  Luckily,
-  this case rarely occurs in practice, because syntax forms to be
-  translated usually correspond to some bits of concrete notation.%
+  written as prefix applications are difficult to make robust.
+  Luckily, this case rarely occurs in practice, because syntax forms
+  to be translated usually correspond to some bits of concrete
+  notation.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -1528,7 +1529,7 @@
   Such syntactic constants are invented on the spot, without formal
   check wrt.\ existing declarations.  It is conventional to use plain
   identifiers prefixed by a single underscore (e.g.\ \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5F}{\isacharunderscore}}foobar{\isaliteral{22}{\isachardoublequote}}}).  Names should be chosen with care, to avoid clashes
-  with unrelated syntax declarations.
+  with other syntax declarations.
 
   \medskip The special case of copy production is specified by \isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}}\verb|""| (empty string).  It means that the
   resulting parse tree \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{22}{\isachardoublequote}}} is copied directly, without any
@@ -1540,7 +1541,7 @@
 
   \item \hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}~\isa{rules} specifies syntactic
   translation rules (i.e.\ macros) as first-order rewrite rules on
-  ASTs (see also \secref{sec:ast}).  The theory context maintains two
+  ASTs (\secref{sec:ast}).  The theory context maintains two
   independent lists translation rules: parse rules (\verb|=>|
   or \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7269676874686172706F6F6E75703E}{\isasymrightharpoonup}}{\isaliteral{22}{\isachardoublequote}}}) and print rules (\verb|<=| or \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C656674686172706F6F6E646F776E3E}{\isasymleftharpoondown}}{\isaliteral{22}{\isachardoublequote}}}).
   For convenience, both can be specified simultaneously as parse~/
@@ -1660,7 +1661,7 @@
   chosen in order of appearance in the theory definitions.
 
   The configuration options \hyperlink{attribute.syntax-ast-trace}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ast{\isaliteral{5F}{\isacharunderscore}}trace}}} and
-  \hyperlink{attribute.syntax-ast-stats}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ast{\isaliteral{5F}{\isacharunderscore}}stats}}} might help understand this process
+  \hyperlink{attribute.syntax-ast-stats}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ast{\isaliteral{5F}{\isacharunderscore}}stats}}} might help to understand this process
   and diagnose problems.
 
   \begin{warn}
@@ -1759,11 +1760,9 @@
   \end{tabular}}
   \medskip
 
-  The argument list consist of \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}c{\isaliteral{2C}{\isacharcomma}}\ tr{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} pairs, where \isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{22}{\isachardoublequote}}} is the syntax name of the syntax constant, term constant or
-  type constructor involved, and \isa{{\isaliteral{22}{\isachardoublequote}}tr{\isaliteral{22}{\isachardoublequote}}} a function that
-  translates a syntax form \isa{{\isaliteral{22}{\isachardoublequote}}c\ args{\isaliteral{22}{\isachardoublequote}}} into \isa{{\isaliteral{22}{\isachardoublequote}}tr\ args{\isaliteral{22}{\isachardoublequote}}}.
-  For print translations, the naming convention for such functions is
-  \isa{{\isaliteral{22}{\isachardoublequote}}tr{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequote}}} instead of \isa{{\isaliteral{22}{\isachardoublequote}}tr{\isaliteral{22}{\isachardoublequote}}}.
+  The argument list consists of \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}c{\isaliteral{2C}{\isacharcomma}}\ tr{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} pairs, where \isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{22}{\isachardoublequote}}} is the syntax name of the formal entity involved, and \isa{{\isaliteral{22}{\isachardoublequote}}tr{\isaliteral{22}{\isachardoublequote}}} a function that translates a syntax form \isa{{\isaliteral{22}{\isachardoublequote}}c\ args{\isaliteral{22}{\isachardoublequote}}} into
+  \isa{{\isaliteral{22}{\isachardoublequote}}tr\ args{\isaliteral{22}{\isachardoublequote}}}.  The ML naming convention for parse translations
+  is \isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{5F}{\isacharunderscore}}tr{\isaliteral{22}{\isachardoublequote}}} and for print translations \isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{5F}{\isacharunderscore}}tr{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequote}}}.
 
   The \indexref{}{command}{print\_syntax}\hyperlink{command.print-syntax}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}syntax}}}} command displays the sets of names
   associated with the translation functions of a theory under \isa{{\isaliteral{22}{\isachardoublequote}}parse{\isaliteral{5F}{\isacharunderscore}}ast{\isaliteral{5F}{\isacharunderscore}}translation{\isaliteral{22}{\isachardoublequote}}} etc.
@@ -1797,7 +1796,7 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-The different kinds of translation functions are called during
+The different kinds of translation functions are invoked during
   the transformations between parse trees, ASTs and syntactic terms
   (cf.\ \figref{fig:parse-print}).  Whenever a combination of the form
   \isa{{\isaliteral{22}{\isachardoublequote}}c\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} is encountered, and a translation function
@@ -1810,7 +1809,8 @@
   the form \verb|Const|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}c{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} or \verb|Const|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}c{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{24}{\isachardollar}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{24}{\isachardollar}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{24}{\isachardollar}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}.  Terms allow more sophisticated transformations
   than ASTs do, typically involving abstractions and bound
   variables. \emph{Typed} print translations may even peek at the type
-  \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} of the constant they are invoked on.
+  \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} of the constant they are invoked on, although that information
+  may be inaccurate.
 
   Regardless of whether they act on ASTs or terms, translation
   functions called during the parsing process differ from those for