src/Pure/General/name_space.ML
changeset 30861 294e8ee163ea
parent 30522 e26b80647189
child 32738 15bb09ca0378
equal deleted inserted replaced
30859:29eb80cef6b7 30861:294e8ee163ea