--- a/doc-src/IsarRef/syntax.tex Sat Dec 09 18:05:34 2006 +0100
+++ b/doc-src/IsarRef/syntax.tex Sat Dec 09 18:05:36 2006 +0100
@@ -435,6 +435,7 @@
prop & : & \isarantiq \\
term & : & \isarantiq \\
const & : & \isarantiq \\
+ abbrev & : & \isarantiq \\
typeof & : & \isarantiq \\
typ & : & \isarantiq \\
thm_style & : & \isarantiq \\
@@ -465,7 +466,7 @@
which are easier to read.
\indexisarant{theory}\indexisarant{thm}\indexisarant{prop}\indexisarant{term}\indexisarant{const}
-\indexisarant{typeof}\indexisarant{typ}\indexisarant{thm-style}
+\indexisarant{abbrev}\indexisarant{typeof}\indexisarant{typ}\indexisarant{thm-style}
\indexisarant{term-style}\indexisarant{text}\indexisarant{goals}
\indexisarant{subgoals}\indexisarant{prf}\indexisarant{full-prf}\indexisarant{ML}
\indexisarant{ML-type}\indexisarant{ML-struct}
@@ -480,6 +481,7 @@
'prop' options prop |
'term' options term |
'const' options term |
+ 'abbrev' options term |
'typeof' options term |
'typ' options type |
'thm\_style' options name thmref |
@@ -517,6 +519,9 @@
\item [$\at\{term~t\}$] prints a well-typed term $t$.
\item [$\at\{const~c\}$] prints a well-defined constant $c$.
+
+\item [$\at\{abbrev~c\,\vec x\}$] prints a constant abbreviation
+ $c\,\vec x \equiv rhs$ as defined in the current context.
\item [$\at\{typeof~t\}$] prints the type of a well-typed term $t$.