src/Pure/Isar/token.ML
changeset 79866 75871d47e400
parent 78819 b8775a63cb35
child 80910 406a85a25189
equal deleted inserted replaced
79863:81717ee51920 79866:75871d47e400