src/Pure/Syntax/syn_ext.ML
changeset 6942 f291292d727c
parent 6760 1c56eb841afe
child 7472 f1208505d837