src/Pure/Syntax/syntax_ext.ML
changeset 62921 499a63c30d55
parent 62808 288c309df28d
child 63806 c54a53ef1873
equal deleted inserted replaced
62920:a5853334c179 62921:499a63c30d55