src/Pure/Syntax/syn_ext.ML
changeset 35114 b1fd1d756e20
parent 35110 dc4f61a7918a
child 35351 7425aece4ee3