# HG changeset patch
# User wenzelm
# Date 1162896476 -3600
# Node ID dbb8decc36bc0d8f92c02272b9cec16708933fc3
# Parent  62ccdaf9369a1e616943d5dca7c7dadff919e6b7
'const_syntax' command: allow fixed variables, renamed to 'notation';

diff -r 62ccdaf9369a -r dbb8decc36bc NEWS
--- a/NEWS	Tue Nov 07 11:46:50 2006 +0100
+++ b/NEWS	Tue Nov 07 11:47:56 2006 +0100
@@ -222,10 +222,10 @@
 syntax translations that should refer to internal constant
 representations independently of name spaces.
 
-* Isar/locales: 'const_syntax' provides a robust interface to the
-'syntax' primitive that also works in a locale context.  Type
-declaration and internal syntactic representation of given constants
-retrieved from the context.
+* Isar/locales: 'notation' provides a robust interface to the 'syntax'
+primitive that also works in a locale context (both for constants and
+fixed variables).  Type declaration and internal syntactic
+representation of given constants retrieved from the context.
 
 * Isar/locales: new derived specification elements 'axiomatization',
 'definition', 'abbreviation', which support type-inference, admit
@@ -259,7 +259,7 @@
 
 Concrete syntax is attached to specified constants in internal form,
 independently of name spaces.  The parse tree representation is
-slightly different -- use 'const_syntax' instead of raw 'syntax', and
+slightly different -- use 'notation' instead of raw 'syntax', and
 'translations' with explicit "CONST" markup to accommodate this.
 
 * Isar/locales: improved parameter handling:
diff -r 62ccdaf9369a -r dbb8decc36bc doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Tue Nov 07 11:46:50 2006 +0100
+++ b/doc-src/IsarRef/generic.tex	Tue Nov 07 11:47:56 2006 +0100
@@ -7,13 +7,13 @@
 \indexisarcmd{axiomatization}
 \indexisarcmd{definition}\indexisaratt{defn}
 \indexisarcmd{abbreviation}
-\indexisarcmd{const-syntax}
+\indexisarcmd{notation}
 \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{const_syntax} & : & \isarkeep{local{\dsh}theory} \\
+  \isarcmd{notation} & : & \isarkeep{local{\dsh}theory} \\
 \end{matharray}
 
 These specification mechanisms provide a slightly more abstract view
@@ -29,7 +29,7 @@
   ;
   'abbreviation' locale? mode? (constdecl? prop +)
   ;
-  'const\_syntax' locale? mode? (nameref mixfix +)
+  'notation' locale? mode? (nameref mixfix +)
   ;
 
   consts: ((name ('::' type)? structmixfix? | vars) + 'and')
@@ -83,11 +83,11 @@
   that affects the concrete syntax declared for abbreviations, cf.\ 
   $\isarkeyword{syntax}$ in \S\ref{sec:syn-trans}.
   
-\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.
+\item $\isarkeyword{notation}~c~mx$ associates mixfix syntax with an
+  existing constant or fixed variable.  This is a robust interface to
+  the underlying $\isarkeyword{syntax}$ primitive
+  (\S\ref{sec:syn-trans}).  Type declaration and internal syntactic
+  representation of the given entity is retrieved from the context.
   
 \end{descr}