src/Pure/Syntax/syn_ext.ML
changeset 4314 a6eb21e10090
parent 4146 00136226f74b
child 4701 be8a8d60d962