src/Pure/General/name_space.ML
changeset 44699 5199ee17c7d7
parent 43560 d1650e3720fd
child 45412 7797f5351ec4