src/Pure/General/name_space.ML
changeset 24854 0ebcd575d3c6
parent 24361 52a14669f9e9
child 25072 03f57b516e12