doc-src/IsarImplementation/Thy/document/Prelim.tex
changeset 30365 790129514c2d
parent 30296 25eb9a499966
child 33174 1f2051f41335
     1.1 --- a/doc-src/IsarImplementation/Thy/document/Prelim.tex	Sun Mar 08 17:26:14 2009 +0100
     1.2 +++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex	Sun Mar 08 17:37:18 2009 +0100
     1.3 @@ -791,11 +791,11 @@
     1.4  %
     1.5  \begin{isamarkuptext}%
     1.6  \begin{mldecls}
     1.7 -  \indexdef{}{ML}{NameSpace.base\_name}\verb|NameSpace.base_name: string -> string| \\
     1.8 -  \indexdef{}{ML}{NameSpace.qualifier}\verb|NameSpace.qualifier: string -> string| \\
     1.9 -  \indexdef{}{ML}{NameSpace.append}\verb|NameSpace.append: string -> string -> string| \\
    1.10 -  \indexdef{}{ML}{NameSpace.implode}\verb|NameSpace.implode: string list -> string| \\
    1.11 -  \indexdef{}{ML}{NameSpace.explode}\verb|NameSpace.explode: string -> string list| \\
    1.12 +  \indexdef{}{ML}{Long\_Name.base\_name}\verb|Long_Name.base_name: string -> string| \\
    1.13 +  \indexdef{}{ML}{Long\_Name.qualifier}\verb|Long_Name.qualifier: string -> string| \\
    1.14 +  \indexdef{}{ML}{Long\_Name.append}\verb|Long_Name.append: string -> string -> string| \\
    1.15 +  \indexdef{}{ML}{Long\_Name.implode}\verb|Long_Name.implode: string list -> string| \\
    1.16 +  \indexdef{}{ML}{Long\_Name.explode}\verb|Long_Name.explode: string -> string list| \\
    1.17    \end{mldecls}
    1.18    \begin{mldecls}
    1.19    \indexdef{}{ML type}{NameSpace.naming}\verb|type NameSpace.naming| \\
    1.20 @@ -815,16 +815,16 @@
    1.21  
    1.22    \begin{description}
    1.23  
    1.24 -  \item \verb|NameSpace.base_name|~\isa{name} returns the base name of a
    1.25 +  \item \verb|Long_Name.base_name|~\isa{name} returns the base name of a
    1.26    qualified name.
    1.27  
    1.28 -  \item \verb|NameSpace.qualifier|~\isa{name} returns the qualifier
    1.29 +  \item \verb|Long_Name.qualifier|~\isa{name} returns the qualifier
    1.30    of a qualified name.
    1.31  
    1.32 -  \item \verb|NameSpace.append|~\isa{name\isactrlisub {\isadigit{1}}\ name\isactrlisub {\isadigit{2}}}
    1.33 +  \item \verb|Long_Name.append|~\isa{name\isactrlisub {\isadigit{1}}\ name\isactrlisub {\isadigit{2}}}
    1.34    appends two qualified names.
    1.35  
    1.36 -  \item \verb|NameSpace.implode|~\isa{name} and \verb|NameSpace.explode|~\isa{names} convert between the packed string
    1.37 +  \item \verb|Long_Name.implode|~\isa{names} and \verb|Long_Name.explode|~\isa{name} convert between the packed string
    1.38    representation and the explicit list form of qualified names.
    1.39  
    1.40    \item \verb|NameSpace.naming| represents the abstract concept of