src/Pure/Syntax/syntax_ext.ML
changeset 42581 398fff2c6b8f
parent 42298 d622145603ee
child 43323 28e71a685c84