changeset 25225 | e638164593bf |
parent 25072 | 03f57b516e12 |
child 26440 | feeb83f9657f |
--- a/src/Pure/General/name_space.ML Mon Oct 29 16:13:43 2007 +0100 +++ b/src/Pure/General/name_space.ML Mon Oct 29 16:13:44 2007 +0100 @@ -20,6 +20,7 @@ sig include BASIC_NAME_SPACE val hidden: string -> string + val is_hidden: string -> bool val separator: string (*single char*) val is_qualified: string -> bool val implode: string list -> string