src/Pure/Syntax/extension.ML
changeset 2383 4127499d9b52
parent 171 ab0f93a291b5
equal deleted inserted replaced
2382:e7c2bce815ba 2383:4127499d9b52