src/Pure/Syntax/syn_ext.ML
changeset 42287 d98eb048a2e4
parent 42268 01401287c3f7