src/Pure/Syntax/syn_ext.ML
changeset 6761 aa71a04f4b93
parent 6760 1c56eb841afe
child 7472 f1208505d837
equal deleted inserted replaced
6760:1c56eb841afe 6761:aa71a04f4b93