--- 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:
--- 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}