doc-src/IsarRef/Thy/Spec.thy
changeset 40256 eb5412b77ac4
parent 40255 9ffbc25e1606
child 40784 177e8cea3e09
     1.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Fri Oct 29 11:49:56 2010 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Fri Oct 29 16:16:10 2010 +0200
     1.3 @@ -322,8 +322,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 `@{text "_"}' 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