src/Pure/Syntax/syntax_ext.ML
changeset 42889 412fe70f41a4
parent 42298 d622145603ee
child 43323 28e71a685c84