src/Pure/Syntax/syntax_ext.ML
changeset 63905 1c3dcb5fe6cb
parent 63806 c54a53ef1873
child 63933 e149e3e320a3