# HG changeset patch
# User wenzelm
# Date 1147808004 -7200
# Node ID eee5e8dbda59e7b3af48b7956837bd27b8d315f5
# Parent  8885951e9c2df70ff2375452919916da53ac9cc7
const_syntax;

diff -r 8885951e9c2d -r eee5e8dbda59 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Tue May 16 21:33:23 2006 +0200
+++ b/doc-src/IsarRef/generic.tex	Tue May 16 21:33:24 2006 +0200
@@ -5,13 +5,16 @@
 
 \subsection{Derived specifications}
 
+\indexisarcmd{axiomatization}
 \indexisarcmd{definition}\indexisaratt{defn}
-\indexisarcmd{abbreviation}\indexisarcmd{axiomatization}
+\indexisarcmd{abbreviation}
+\indexisarcmd{const-syntax}
 \begin{matharray}{rcll}
+  \isarcmd{axiomatization} & : & \isarkeep{local{\dsh}theory} & (axiomatic!)\\
   \isarcmd{definition} & : & \isarkeep{local{\dsh}theory} \\
   defn & : & \isaratt \\
   \isarcmd{abbreviation} & : & \isarkeep{local{\dsh}theory} \\
-  \isarcmd{axiomatization} & : & \isarkeep{local{\dsh}theory} & (axiomatic!)\\
+  \isarcmd{const_syntax} & : & \isarkeep{local{\dsh}theory} \\
 \end{matharray}
 
 These specification mechanisms provide a slightly more abstract view
@@ -21,12 +24,13 @@
 available, and result names need not be given.
 
 \begin{rail}
+  'axiomatization' locale? consts? ('where' specs)?
+  ;
   'definition' locale? (constdecl? constdef +)
   ;
-
   'abbreviation' locale? mode? (constdecl? prop +)
   ;
-  'axiomatization' locale? consts? ('where' specs)?
+  'const\_syntax' locale? mode? (nameref mixfix +)
   ;
 
   consts: ((name ('::' type)? structmixfix? | vars) + 'and')
@@ -37,6 +41,16 @@
 
 \begin{descr}
   
+\item $\isarkeyword{axiomatization} ~ c@1 \dots c@n ~
+  \isarkeyword{where} ~ A@1 \dots A@m$ introduces several constants
+  simultaneously and states axiomatic properties for these.  The
+  constants are marked as being specified once and for all, which
+  prevents additional specifications being issued later on.
+  
+  Note that axiomatic specifications are only appropriate when
+  declaring a new logical system.  Normal applications should only use
+  definitional mechanisms!
+
 \item $\isarkeyword{definition}~c~\isarkeyword{where}~eq$ produces an
   internal definition $c \equiv t$ according to the specification
   given as $eq$, which is then turned into a proven fact.  The given
@@ -70,16 +84,12 @@
   that affects the concrete syntax declared for abbreviations, cf.\ 
   $\isarkeyword{syntax}$ in \S\ref{sec:syn-trans}.
   
-\item $\isarkeyword{axiomatization} ~ c@1 \dots c@n ~
-  \isarkeyword{where} ~ A@1 \dots A@m$ introduces several constants
-  simultaneously and states axiomatic properties for these.  The
-  constants are marked as being specified once and for all, which
-  prevents additional specifications being issued later on.
+\item $\isarkeyword{const_syntax}~c~mx$ associates mixfix syntax with
+  an existing constant $c$.  This is a robust interface to the
+  underlying $\isarkeyword{syntax}$ primitive (\S\ref{sec:syn-trans}).
+  Type declaration and internal syntactic representation of given
+  constants is retrieved from the context.
   
-  Note that axiomatic specifications are only appropriate when
-  declaring a new logical system.  Normal applications should only use
-  definitional mechanisms!
-
 \end{descr}
 
 Any of these specifications support an optional target locale context