src/Pure/General/name_space.ML
changeset 6118 caa439435666
parent 5682 9125611c1645
child 6845 598d2f32d452
equal deleted inserted replaced
6117:f9aad8ccd590 6118:caa439435666
     1 (*  Title:      Pure/name_space.ML
     1 (*  Title:      Pure/General/name_space.ML
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     4 
     5 Hierarchically structured name spaces.
     5 Hierarchically structured name spaces.
     6 
     6