src/Pure/Isar/token.ML
changeset 69227 71b48b749836
parent 68730 0bc491938780
child 69851 29a4f633609e
equal deleted inserted replaced
69226:68f5dc2275ac 69227:71b48b749836