doc-src/IsarImplementation/Thy/prelim.thy
 changeset 26872 336dfd860744 parent 26864 1417e704d724 child 29008 d863c103ded0
equal 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