src/Pure/Syntax/syn_ext.ML
changeset 7217 3af1e69b25b8
parent 6760 1c56eb841afe
child 7472 f1208505d837