src/Pure/Syntax/syn_ext.ML
changeset 35111 18cd034922ba
parent 35110 dc4f61a7918a
child 35351 7425aece4ee3