src/Pure/Syntax/syn_ext.ML
changeset 554 c7d9018cc9e6
parent 441 2b97bd6415b7
child 555 a7f397a14b16