# HG changeset patch
# User wenzelm
# Date 1328637082 -3600
# Node ID f248b5f2783adea21fd37b06c84f5807e0d57459
# Parent  4eb48958b50f48f03baa795cecd0361cc1228ab1
updated examples for syntax translations;

diff -r 4eb48958b50f -r f248b5f2783a doc-src/IsarRef/Thy/Inner_Syntax.thy
--- 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}
 *}
 
 
diff -r 4eb48958b50f -r f248b5f2783a doc-src/IsarRef/Thy/document/Inner_Syntax.tex
--- 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%
 %
diff -r 4eb48958b50f -r f248b5f2783a doc-src/Ref/Makefile
--- 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
 
diff -r 4eb48958b50f -r f248b5f2783a doc-src/Ref/defining.tex
--- 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: 
diff -r 4eb48958b50f -r f248b5f2783a doc-src/Ref/ref.tex
--- 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}