--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Sun Feb 05 21:00:38 2012 +0100
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Tue Feb 07 18:51:22 2012 +0100
@@ -1118,6 +1118,27 @@
@{command "translations"} above.
\end{description}
+
+ Raw syntax and translations provides a slightly more low-level
+ access to the grammar and the form of resulting parse trees. It is
+ often possible to avoid this untyped macro mechanism, and use
+ type-safe @{command abbreviation} or @{command notation} instead.
+ Some important situations where @{command syntax} and @{command
+ translations} are really need are as follows:
+
+ \begin{itemize}
+
+ \item Iterated replacement via recursive @{command translations}.
+ For example, consider list enumeration @{term "[a, b, c, d]"} as
+ defined in theory @{theory List} in Isabelle/HOL.
+
+ \item Change of binding status of variables: anything beyond the
+ built-in @{keyword "binder"} mixfix annotation requires explicit
+ syntax translations. For example, consider list filter
+ comprehension @{term "[x \<leftarrow> xs . P]"} as defined in theory @{theory
+ List} in Isabelle/HOL.
+
+ \end{itemize}
*}
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Sun Feb 05 21:00:38 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Tue Feb 07 18:51:22 2012 +0100
@@ -1346,7 +1346,26 @@
translation rules, which are interpreted in the same manner as for
\hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}} above.
- \end{description}%
+ \end{description}
+
+ Raw syntax and translations provides a slightly more low-level
+ access to the grammar and the form of resulting parse trees. It is
+ often possible to avoid this untyped macro mechanism, and use
+ type-safe \hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}} or \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}} instead.
+ Some important situations where \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} and \hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}} are really need are as follows:
+
+ \begin{itemize}
+
+ \item Iterated replacement via recursive \hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}.
+ For example, consider list enumeration \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{2C}{\isacharcomma}}\ c{\isaliteral{2C}{\isacharcomma}}\ d{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} as
+ defined in theory \hyperlink{theory.List}{\mbox{\isa{List}}} in Isabelle/HOL.
+
+ \item Change of binding status of variables: anything beyond the
+ built-in \hyperlink{keyword.binder}{\mbox{\isa{\isakeyword{binder}}}} mixfix annotation requires explicit
+ syntax translations. For example, consider list filter
+ comprehension \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}x\ {\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}\ xs\ {\isaliteral{2E}{\isachardot}}\ P{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} as defined in theory \hyperlink{theory.List}{\mbox{\isa{List}}} in Isabelle/HOL.
+
+ \end{itemize}%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/Ref/Makefile Sun Feb 05 21:00:38 2012 +0100
+++ b/doc-src/Ref/Makefile Tue Feb 07 18:51:22 2012 +0100
@@ -9,7 +9,7 @@
include ../Makefile.in
NAME = ref
-FILES = ref.tex tactic.tex thm.tex defining.tex syntax.tex \
+FILES = ref.tex tactic.tex thm.tex syntax.tex \
substitution.tex simplifier.tex classical.tex ../proof.sty \
../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
--- a/doc-src/Ref/defining.tex Sun Feb 05 21:00:38 2012 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-
-\chapter{Defining Logics} \label{Defining-Logics}
-
-\section{Mixfix declarations} \label{sec:mixfix}
-
-\subsection{Example: arithmetic expressions}
-\index{examples!of mixfix declarations}
-This theory specification contains a {\tt syntax} section with mixfix
-declarations encoding the priority grammar from
-\S\ref{sec:priority_grammars}:
-\begin{ttbox}
-ExpSyntax = Pure +
-types
- exp
-syntax
- "0" :: exp ("0" 9)
- "+" :: [exp, exp] => exp ("_ + _" [0, 1] 0)
- "*" :: [exp, exp] => exp ("_ * _" [3, 2] 2)
- "-" :: exp => exp ("- _" [3] 3)
-end
-\end{ttbox}
-Executing {\tt Syntax.print_gram} reveals the productions derived from the
-above mixfix declarations (lots of additional information deleted):
-\begin{ttbox}
-Syntax.print_gram (syn_of ExpSyntax.thy);
-{\out exp = "0" => "0" (9)}
-{\out exp = exp[0] "+" exp[1] => "+" (0)}
-{\out exp = exp[3] "*" exp[2] => "*" (2)}
-{\out exp = "-" exp[3] => "-" (3)}
-\end{ttbox}
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "ref"
-%%% End:
--- a/doc-src/Ref/ref.tex Sun Feb 05 21:00:38 2012 +0100
+++ b/doc-src/Ref/ref.tex Tue Feb 07 18:51:22 2012 +0100
@@ -49,7 +49,6 @@
\include{tactic}
\include{thm}
-\include{defining}
\include{syntax}
\include{substitution}
\include{simplifier}