src/Pure/Syntax/syn_ext.ML
changeset 7346 dace49c16aca
parent 6760 1c56eb841afe
child 7472 f1208505d837