src/Pure/General/name_space.ML
changeset 44502 c537d5e5a365
parent 43560 d1650e3720fd
child 45412 7797f5351ec4
equal deleted inserted replaced
44501:5bde887b4785 44502:c537d5e5a365