Namespace element
Keywords: namespace
A namespace element is a namespace definition, which might be preceded by a block introduction.
Definition:
ns_element := [block_intro(*)] ns_definition
A namespace element is a namespace definition, which might be preceded by a block introduction.
ns_element := [block_intro(*)] ns_definition