src/Pure/General/name_space.ML
changeset 45107 76fef3e57004
parent 43560 d1650e3720fd
child 45412 7797f5351ec4