export is_hidden;
authorwenzelm
Mon Oct 29 16:13:44 2007 +0100 (2007-10-29)
changeset 25225e638164593bf
parent 25224 6d4d26e878f4
child 25226 502d8676cdd6
export is_hidden;
src/Pure/General/name_space.ML
     1.1 --- a/src/Pure/General/name_space.ML	Mon Oct 29 16:13:43 2007 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Mon Oct 29 16:13:44 2007 +0100
     1.3 @@ -20,6 +20,7 @@
     1.4  sig
     1.5    include BASIC_NAME_SPACE
     1.6    val hidden: string -> string
     1.7 +  val is_hidden: string -> bool
     1.8    val separator: string                 (*single char*)
     1.9    val is_qualified: string -> bool
    1.10    val implode: string list -> string