--- a/doc-src/IsarRef/Thy/document/Spec.tex Fri Oct 29 11:49:56 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Fri Oct 29 16:16:10 2010 +0200
@@ -346,8 +346,8 @@
A locale instance consists of a reference to a locale and either
positional or named parameter instantiations. Identical
instantiations (that is, those that instante a parameter by itself)
- may be omitted. The notation `\_' enables to omit the instantiation
- for a parameter inside a positional instantiation.
+ may be omitted. The notation `\isa{{\isachardoublequote}{\isacharunderscore}{\isachardoublequote}}' enables to omit the
+ instantiation for a parameter inside a positional instantiation.
Terms in instantiations are from the context the locale expressions
is declared in. Local names may be added to this context with the