doc-src/IsarImplementation/Thy/prelim.thy
changeset 21862 13e9febe3080
parent 21852 7f2853bd54bf
child 22438 96e650157b1e
equal deleted inserted replaced
21861:a972053ed147 21862:13e9febe3080
   700 text %mlref {*
   700 text %mlref {*
   701   \begin{mldecls}
   701   \begin{mldecls}
   702   @{index_ML NameSpace.base: "string -> string"} \\
   702   @{index_ML NameSpace.base: "string -> string"} \\
   703   @{index_ML NameSpace.qualifier: "string -> string"} \\
   703   @{index_ML NameSpace.qualifier: "string -> string"} \\
   704   @{index_ML NameSpace.append: "string -> string -> string"} \\
   704   @{index_ML NameSpace.append: "string -> string -> string"} \\
   705   @{index_ML NameSpace.pack: "string list -> string"} \\
   705   @{index_ML NameSpace.implode: "string list -> string"} \\
   706   @{index_ML NameSpace.unpack: "string -> string list"} \\
   706   @{index_ML NameSpace.explode: "string -> string list"} \\
   707   \end{mldecls}
   707   \end{mldecls}
   708   \begin{mldecls}
   708   \begin{mldecls}
   709   @{index_ML_type NameSpace.naming} \\
   709   @{index_ML_type NameSpace.naming} \\
   710   @{index_ML NameSpace.default_naming: NameSpace.naming} \\
   710   @{index_ML NameSpace.default_naming: NameSpace.naming} \\
   711   @{index_ML NameSpace.add_path: "string -> NameSpace.naming -> NameSpace.naming"} \\
   711   @{index_ML NameSpace.add_path: "string -> NameSpace.naming -> NameSpace.naming"} \\
   729   of a qualified name.
   729   of a qualified name.
   730 
   730 
   731   \item @{ML NameSpace.append}~@{text "name\<^isub>1 name\<^isub>2"}
   731   \item @{ML NameSpace.append}~@{text "name\<^isub>1 name\<^isub>2"}
   732   appends two qualified names.
   732   appends two qualified names.
   733 
   733 
   734   \item @{ML NameSpace.pack}~@{text "name"} and @{ML
   734   \item @{ML NameSpace.implode}~@{text "name"} and @{ML
   735   NameSpace.unpack}~@{text "names"} convert between the packed string
   735   NameSpace.explode}~@{text "names"} convert between the packed string
   736   representation and the explicit list form of qualified names.
   736   representation and the explicit list form of qualified names.
   737 
   737 
   738   \item @{ML_type NameSpace.naming} represents the abstract concept of
   738   \item @{ML_type NameSpace.naming} represents the abstract concept of
   739   a naming policy.
   739   a naming policy.
   740 
   740