src/Pure/name.ML
changeset 32738 15bb09ca0378
parent 31035 de0a20a030fd
child 33095 bbd52d2f8696
equal deleted inserted replaced
32737:76fa673eee8b 32738:15bb09ca0378