equal
deleted
inserted
replaced
320 \end{rail} |
320 \end{rail} |
321 |
321 |
322 A locale instance consists of a reference to a locale and either |
322 A locale instance consists of a reference to a locale and either |
323 positional or named parameter instantiations. Identical |
323 positional or named parameter instantiations. Identical |
324 instantiations (that is, those that instante a parameter by itself) |
324 instantiations (that is, those that instante a parameter by itself) |
325 may be omitted. The notation `\_' enables to omit the instantiation |
325 may be omitted. The notation `@{text "_"}' enables to omit the |
326 for a parameter inside a positional instantiation. |
326 instantiation for a parameter inside a positional instantiation. |
327 |
327 |
328 Terms in instantiations are from the context the locale expressions |
328 Terms in instantiations are from the context the locale expressions |
329 is declared in. Local names may be added to this context with the |
329 is declared in. Local names may be added to this context with the |
330 optional for clause. In addition, syntax declarations from one |
330 optional for clause. In addition, syntax declarations from one |
331 instance are effective when parsing subsequent instances of the same |
331 instance are effective when parsing subsequent instances of the same |