src/Pure/General/name_space.ML
changeset 81519 cdc43c0fdbfc
parent 80298 f3bfec3b02f0
child 81531 b224e42b66f5
equal deleted inserted replaced
81518:f012cbfd96d0 81519:cdc43c0fdbfc