src/Pure/Syntax/syn_ext.ML
changeset 29270 0eade173f77e
parent 28904 3ef9489eeef5
child 29318 6337d1cb2ba0