eliminated obsolete \_ escape;
authorwenzelm
Fri Oct 29 16:16:10 2010 +0200 (2010-10-29)
changeset 40256eb5412b77ac4
parent 40255 9ffbc25e1606
child 40270 56e705fc8fdb
eliminated obsolete \_ escape;
doc-src/IsarRef/Thy/Spec.thy
doc-src/IsarRef/Thy/document/Spec.tex
     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
     2.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Fri Oct 29 11:49:56 2010 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Fri Oct 29 16:16:10 2010 +0200
     2.3 @@ -346,8 +346,8 @@
     2.4    A locale instance consists of a reference to a locale and either
     2.5    positional or named parameter instantiations.  Identical
     2.6    instantiations (that is, those that instante a parameter by itself)
     2.7 -  may be omitted.  The notation `\_' enables to omit the instantiation
     2.8 -  for a parameter inside a positional instantiation.
     2.9 +  may be omitted.  The notation `\isa{{\isachardoublequote}{\isacharunderscore}{\isachardoublequote}}' enables to omit the
    2.10 +  instantiation for a parameter inside a positional instantiation.
    2.11  
    2.12    Terms in instantiations are from the context the locale expressions
    2.13    is declared in.  Local names may be added to this context with the