author | wenzelm |
Wed, 01 Oct 1997 18:19:18 +0200 | |
changeset 3769 | 931c336b0707 |
parent 3768 | 67f4ac759100 |
child 3770 | 294b5905f4eb |
--- a/src/Pure/name_space.ML Wed Oct 01 18:13:41 1997 +0200 +++ b/src/Pure/name_space.ML Wed Oct 01 18:19:18 1997 +0200 @@ -11,6 +11,7 @@ signature NAME_SPACE = sig + val separator: string (*single char!*) val unpack: string -> string list val pack: string list -> string val qualified: string -> bool