src/Pure/Syntax/extension.ML
changeset 4567 b0b963a01a0c
parent 171 ab0f93a291b5
equal deleted inserted replaced
4566:23c01c724d7a 4567:b0b963a01a0c