src/Pure/Syntax/syntax_ext.ML
changeset 63429 baedd4724f08
parent 62808 288c309df28d
child 63806 c54a53ef1873
equal deleted inserted replaced
63428:005b490f0ce2 63429:baedd4724f08