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