doc-src/IsarRef/Thy/document/Spec.tex
changeset 40256 eb5412b77ac4
parent 40255 9ffbc25e1606
child 40406 313a24b66a8d
     1.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Fri Oct 29 11:49:56 2010 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Fri Oct 29 16:16:10 2010 +0200
     1.3 @@ -346,8 +346,8 @@
     1.4    A locale instance consists of a reference to a locale and either
     1.5    positional or named parameter instantiations.  Identical
     1.6    instantiations (that is, those that instante a parameter by itself)
     1.7 -  may be omitted.  The notation `\_' enables to omit the instantiation
     1.8 -  for a parameter inside a positional instantiation.
     1.9 +  may be omitted.  The notation `\isa{{\isachardoublequote}{\isacharunderscore}{\isachardoublequote}}' enables to omit the
    1.10 +  instantiation for a parameter inside a positional instantiation.
    1.11  
    1.12    Terms in instantiations are from the context the locale expressions
    1.13    is declared in.  Local names may be added to this context with the