equal
deleted
inserted
replaced
402 |
402 |
403 \end{description} |
403 \end{description} |
404 *} |
404 *} |
405 |
405 |
406 |
406 |
407 section {* Names *} |
407 section {* Names \label{sec:names} *} |
408 |
408 |
409 text {* |
409 text {* |
410 In principle, a name is just a string, but there are various |
410 In principle, a name is just a string, but there are various |
411 convention for encoding additional structure. For example, ``@{text |
411 convention for encoding additional structure. For example, ``@{text |
412 "Foo.bar.baz"}'' is considered as a qualified name consisting of |
412 "Foo.bar.baz"}'' is considered as a qualified name consisting of |